Logically atomic triples conflict with autosubst notation
Autosubst uses >>
and >>>
as notation for some operations, which conflicts with our logically atomic triples:
Section notation_conflicts.
Context `{!heapGS Σ}.
(* Test compatibility with autosubst notation. *)
Reserved Notation "f >>> g" (at level 56, left associativity).
Reserved Notation "sigma >> tau" (at level 56, left associativity).
Lemma conflict_test1 P Q e v :
⊢ <<< P >>> e @ ∅ <<< Q, RET v >>>.
(* Syntax error: '>>>' expected after [term level 200] (in [term]) *)
I tried changing the '>>>'
in our notations to >>>
or to '>' '>' '>'
, neither of that helped. (We are using } } }
for texan triples, I have no idea why.) I also tried removing the level declarations from the logatom triples, again that made no difference. I don't actually understand what is happening here anyway, these were complete shots in the dark.
We need someone who actually understand the Coq notation system for this... maybe @Blaisorblade?