Syntax with backticks

Using Coq
1

I’m trying to compile old Coq code with a new version and I can’t figure out how change (or make compilable) the code with backticks.

    Inductive avl : tree -> Prop :=
    | RBLeaf : avl Leaf
    | RBNode : forall (x :elt) (l r :tree) (h:Z),
        avl l -> avl r ->
        `-2 <= (height l) - (height r) <= 2` ->
        height_of_node l r h ->
        avl (Node l x r h).
  1. How to repair this code?
  2. If it is a custom notation how can I list available notations or “google” it properly? (I found only this which seems not to be relevant…)
2

Just remove the backticks.

1 Like