# Syntax with backticks

**URL:** <https://discourse.rocq-prover.org/t/syntax-with-backticks/1231>\
**Category:** Using Rocq\
**Created:** [March 11, 2021, 8:38pm UTC](https://discourse.rocq-prover.org/t/syntax-with-backticks/1231 "2021-03-11T20:38:24Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![Kakadu](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/kakadu/32/217_2.png) [@Kakadu](https://discourse.rocq-prover.org/u/Kakadu)\
**Post date:** [March 11, 2021, 8:38pm UTC](https://discourse.rocq-prover.org/t/syntax-with-backticks/1231/1 "2021-03-11T20:38:24Z")

</div>

I’m trying to compile [old Coq code](https://www.lri.fr/~filliatr/fsets/coq/FSetAVL.html) with a new version and I can’t figure out how change (or make compilable) the code with backticks.

```coq
    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](https://coq-club.inria.narkive.com/VxGJ1Tl2/why-backtick-notation-is-needed) which seems not to be relevant…)

---

<div class="post-metadata">

**Author:** ![silene](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/silene/32/485_2.png) [@silene](https://discourse.rocq-prover.org/u/silene)\
**Post date:** [March 11, 2021, 8:44pm UTC](https://discourse.rocq-prover.org/t/syntax-with-backticks/1231/2 "2021-03-11T20:44:54Z")

</div>

Just remove the backticks.