diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_8364.v | 17 | ||||
| -rw-r--r-- | test-suite/modules/Nat.v | 2 |
2 files changed, 18 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_8364.v b/test-suite/bugs/closed/bug_8364.v new file mode 100644 index 0000000000..10f955b41f --- /dev/null +++ b/test-suite/bugs/closed/bug_8364.v @@ -0,0 +1,17 @@ +Unset Primitive Projections. + +Record Box (A:Type) := box { unbox : A }. +Arguments box {_} _. Arguments unbox {_} _. + +Definition map {A B} (f:A -> B) x := + match x with box x => box (f x) end. + +Definition tuple (l : Box Type) : Type := + match l with + | box x => x + end. + +Fail Inductive stack : Type -> Type := +| Stack T foos : + tuple (map stack foos) -> + stack T. diff --git a/test-suite/modules/Nat.v b/test-suite/modules/Nat.v index d2116d2183..95daa1bb0c 100644 --- a/test-suite/modules/Nat.v +++ b/test-suite/modules/Nat.v @@ -2,7 +2,7 @@ Definition T := nat. Definition le := le. -Hint Unfold le. +Hint Unfold le : core. Lemma le_refl : forall n : nat, le n n. auto. |