diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /test-suite/bugs/closed/5762.v | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'test-suite/bugs/closed/5762.v')
-rw-r--r-- | test-suite/bugs/closed/5762.v | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v new file mode 100644 index 00000000..55d36bd7 --- /dev/null +++ b/test-suite/bugs/closed/5762.v @@ -0,0 +1,34 @@ +(* Supporting imp. params. in inductive or fixpoints mutually defined with a notation *) + +Reserved Notation "* a" (at level 70). +Inductive P {n : nat} : nat -> Prop := +| c m : *m +where "* m" := (P m). + +Reserved Notation "##". +Inductive I {A:Type} := C : ## where "##" := I. + +(* The following was working in 8.6 *) + +Require Import Vector. + +Reserved Notation "# a" (at level 70). +Fixpoint f {n : nat} (v:Vector.t nat n) : nat := + match v with + | nil _ => 0 + | cons _ _ _ v => S (#v) + end +where "# v" := (f v). + +(* The following was working in 8.6 *) + +Reserved Notation "%% a" (at level 70). +Record R := + {g : forall {A} (a:A), a=a where "%% x" := (g x); + k : %% 0 = eq_refl}. + +(* An extra example *) + +Module A. +Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I) : I_scope. +End A. |