Question: importing twice breaks notation
Closed this issue · 3 comments
Importing ITree
twice breaks the monadic notation (_ <- _ ;; _
).
Surprisingly, re-importing ITreeNotations
does not fix the problem.
Below is the minimal code. (Checked with Coq 8.12.2 / itree 3.2.0)
From ITree Require Import ITree.
(* Check (x <- Ret 0;; Ret x). *) (** no parsing, no printing **)
Import ITreeNotations.
Check (x <- Ret 0;; Ret x). (** parsing ok, printing ok **)
From ITree Require Import ITree.
Check (x <- Ret 0;; Ret x). (** parsing ok, no printing **)
Import ITreeNotations.
Check (x <- Ret 0;; Ret x). (** parsing ok, no printing **)
It is not an issue in my development, but I just wanted to report it and possibly understand why it happens.
That's odd. This seems to have been fixed in Coq 8.13.
Coq 8.13 output:
x <- Ret 0;; Ret x
: itree ?E nat
where
?E : [ |- Type -> Type]
x <- Ret 0;; Ret x
: itree ?E nat
where
?E : [ |- Type -> Type]
x <- Ret 0;; Ret x
: itree ?E nat
where
?E : [ |- Type -> Type]
Coq 8.12 output:
x <- Ret 0;; Ret x
: itree ?E nat
where
?E : [ |- Type -> Type]
ITree.bind (Ret 0) (fun x : nat => Ret x)
: itree ?E nat
where
?E : [ |- Type -> Type]
ITree.bind (Ret 0) (fun x : nat => Ret x)
: itree ?E nat
where
?E : [ |- Type -> Type]
The changelog of Coq 8.13 mentions some relevant updates in notations, in particular this one (though I don't really get the details):
Changed: Redeclaring a notation also reactivates its printing rule; in particular a second
Import
of the same module reactivates the printing rules declared in this module.
So this seems likely to have been fixed.