summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/shouldsucceed/2021.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2021.v')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2021.v23
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2021.v b/test-suite/bugs/closed/shouldsucceed/2021.v
new file mode 100644
index 00000000..e598e5ae
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2021.v
@@ -0,0 +1,23 @@
+(* correct failure of injection/discriminate on types whose inductive
+ status derives from the substitution of an argument *)
+
+Inductive t : nat -> Type :=
+| M : forall n: nat, nat -> t n.
+
+Lemma eq_t : forall n n' m m',
+ existT (fun B : Type => B) (t n) (M n m) =
+ existT (fun B : Type => B) (t n') (M n' m') -> True.
+Proof.
+ intros.
+ injection H.
+ intro Ht.
+ exact I.
+Qed.
+
+Lemma eq_t' : forall n n' : nat,
+ existT (fun B : Type => B) (t n) (M n 0) =
+ existT (fun B : Type => B) (t n') (M n' 1) -> True.
+Proof.
+ intros.
+ discriminate H || exact I.
+Qed.