Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/dune

Last active November 27, 2021 20:17
Show Gist options
  • Save Blaisorblade/88c97afd74d156d8797f6f2c7b9faaf7 to your computer and use it in GitHub Desktop.
Save Blaisorblade/88c97afd74d156d8797f6f2c7b9faaf7 to your computer and use it in GitHub Desktop.
Download ZIP
Evidence for https://github.com/coq/coq/issues/15255; build by clone + dune build
Raw
dune
(coq.theory
(name notation_test)
(flags (:standard)))
Raw
dune-project
(lang dune 2.9)
(using coq 0.3)
Raw
test1.v
Reserved Notation "L '.=' j" (at level 49, left associativity).
Raw
test2.v
(* Fails *)
From notation_test Require Import test1.
(* From notation_test Require Export test1. *)
Reserved Notation "'<obj>_{' L '}' P" (at level 49).
Raw
test3.v
(* V1: Works. *)
(* From notation_test Require Import test1. *)
(* Print Grammar constr. *)
(* | "49" LEFTA
[ SELF; ".="; NEXT ] *)
(* From notation_test Require Import test2. *)
(* Print Grammar constr. *)
(* | "49" LEFTA
[ SELF; ".="; NEXT
| "<obj>_{"; term LEVEL "200"; "}"; NEXT ] *)
(* V2: Fails, if test2 doesn't import test1, or if it does. *)
From notation_test Require Import test2.
(* Print Grammar constr. *)
(*
| "49" RIGHTA
[ "<obj>_{"; term LEVEL "200"; "}"; NEXT ]
*)
From notation_test Require Import test1.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment