# What are the rules for shadowing Ltac2 tactics?

**URL:** <https://discourse.rocq-prover.org/t/what-are-the-rules-for-shadowing-ltac2-tactics/358>\
**Category:** Using Rocq\
**Tags:** ltac2\
**Created:** [July 16, 2019, 11:27pm UTC](https://discourse.rocq-prover.org/t/what-are-the-rules-for-shadowing-ltac2-tactics/358 "2019-07-16T23:27:07Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![SCappella](https://avatars.discourse-cdn.com/v4/letter/s/46a35a/32.png) [@SCappella](https://discourse.rocq-prover.org/u/SCappella)\
**Post date:** [July 16, 2019, 11:27pm UTC](https://discourse.rocq-prover.org/t/what-are-the-rules-for-shadowing-ltac2-tactics/358/1 "2019-07-16T23:27:07Z")

</div>

First, a bit of background about my motivations. I’m using the `-noinit` option (with manual loading of certain plugins to re-enable tactics), so certain basic tactics don’t really work. One such set of tactics is `reflexivity`, `symmetry` and `transitivity`. If run (in an otherwise valid proof state), we get something along the lines of

`Tactic failure: The relation R is not a declared reflexive relation. Maybe you need to require the Coq.Classes.RelationClasses library.`

which obviously doesn’t work very well in a `-noinit` environment (unless I wanted to pull in a good chunk of the standard library).

What worked with Ltac1 was simply defining new tactics to override these three. I tried doing the same thing with Ltac2, and I came across a situation that I find confusing. This example works without `-noinit`. For the sake of reproducibility, I’m using the master branch of Coq (commit [a5998b06ccf2367f7d1e58dc80e4237754c953bc](https://github.com/coq/coq/tree/a5998b06ccf2367f7d1e58dc80e4237754c953bc)).

```auto
Require Import Ltac2.Ltac2.

Ltac2 reflexivity0 () := Message.print (Message.of_string "Successfully overridden").
Ltac2 Notation reflexivity := reflexivity0 ().
Ltac2 symmetry0 () := Message.print (Message.of_string "Successfully overridden").
Ltac2 Notation symmetry := symmetry0 ().

Goal forall {A: Type} (R: A -> A -> Type) (x: A), R x x.
Proof.
    reflexivity. (* Prints "Successfully overridden" *)
    Fail symmetry. (* Prints the error message from the standard `symmetry` *)
Abort.

```

As you can see, `reflexivity` gets overridden with the new tactic, but `symmetry` still uses the old one. I’ve tried lots of variations here (like directly using `Ltac2 symmetry () := Message.print (Message.of_string "Successfully overridden").` and calling it with `symmetry ().`), but nothing (other than using a different name) seemed to work.

I figured out that the clash comes from Ltac2.Notations.v where we have

```auto
Ltac2 Notation reflexivity := Std.reflexivity ().

Ltac2 symmetry0 cl :=
  Std.symmetry (default_on_concl cl).

Ltac2 Notation "symmetry" cl(opt(clause)) := symmetry0 cl.
Ltac2 Notation symmetry := symmetry.

```

So I’m wondering why this allows `reflexivity` to be overridden with a notation, but not `symmetry`. Is it because using `Ltac2 Notation "string" := _` puts the string in the grammar (and it can’t be removed)? Is there way to print the current state of the Ltac2 grammar (similar to `Print Grammar constr.`) so I can check?

---

<div class="post-metadata">

**Author:** ![ppedrot](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ppedrot/32/55_2.png) [@ppedrot](https://discourse.rocq-prover.org/u/ppedrot)\
**Post date:** [July 19, 2019, 3:00pm UTC](https://discourse.rocq-prover.org/t/what-are-the-rules-for-shadowing-ltac2-tactics/358/2 "2019-07-19T15:00:53Z")

</div>

There are two types of notations in Ltac2, which by design do not rely on the same mechanism.

- Actual notations, like `Ltac2 Notation "symmetry" cl(opt(clause)) := ...`.
- So called syntactic notations, like `Ltac2 Notation symmetry := ...`.

The first one extends the Coq parser with a dedicated rule, which is expanded at parsing time, while the second one is just resolved as a special name (similarly to Gallina’s syntactic notations) whose body is expanded a typing time, i.e. after parsing.

The first kind is more powerful, but is much less modular. It’s easy to wreak havoc at a distance by merely introducing a parsing conflict without really realizing. The second kind is weaker, but as it doesn’t mess with the parser, you can use it safely without second thought.

Here, you’re typically encountering a parsing issue. The standard Ltac notations are using the parsing mechanism, so the syntactic notation doesn’t even have time to fire, it doesn’t parse at all.