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).
- How to repair this code?
- 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…)