diff options
Diffstat (limited to 'test-suite/bugs/closed/5762.v')
| -rw-r--r-- | test-suite/bugs/closed/5762.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v index edd5c8d73..55d36bd72 100644 --- a/test-suite/bugs/closed/5762.v +++ b/test-suite/bugs/closed/5762.v @@ -26,3 +26,9 @@ 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. |