diff options
Diffstat (limited to 'test-suite/bugs')
| -rw-r--r-- | test-suite/bugs/closed/2016.v | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/2021.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_047.v | 2 |
3 files changed, 8 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v index 13ec5bea9b..536e6fabd9 100644 --- a/test-suite/bugs/closed/2016.v +++ b/test-suite/bugs/closed/2016.v @@ -1,6 +1,8 @@ (* Coq 8.2beta4 *) Require Import Classical_Prop. +Unset Structural Injection. + Record coreSemantics : Type := CoreSemantics { core: Type; corestep: core -> core -> Prop; @@ -49,7 +51,7 @@ unfold oe_corestep; intros. assert (HH:= step_fun _ _ _ H H0); clear H H0. destruct q1; destruct q2; unfold oe2coreSem; simpl in *. generalize (inj_pairT1 _ _ _ _ _ _ HH); clear HH; intros. -injection H; clear H; intros. +injection H. revert in_q1 in_corestep1 in_corestep_fun1 H. pattern in_core1. @@ -59,4 +61,4 @@ apply sym_eq. (** good to here **) Show Universes. Print Universes. -Fail apply H0.
\ No newline at end of file +Fail apply H0. diff --git a/test-suite/bugs/closed/2021.v b/test-suite/bugs/closed/2021.v index e598e5aed7..5df92998e1 100644 --- a/test-suite/bugs/closed/2021.v +++ b/test-suite/bugs/closed/2021.v @@ -1,6 +1,8 @@ (* correct failure of injection/discriminate on types whose inductive status derives from the substitution of an argument *) +Unset Structural Injection. + Inductive t : nat -> Type := | M : forall n: nat, nat -> t n. diff --git a/test-suite/bugs/closed/HoTT_coq_047.v b/test-suite/bugs/closed/HoTT_coq_047.v index 29496be5ee..bef3c33ca1 100644 --- a/test-suite/bugs/closed/HoTT_coq_047.v +++ b/test-suite/bugs/closed/HoTT_coq_047.v @@ -1,3 +1,5 @@ +Unset Structural Injection. + Inductive nCk : nat -> nat -> Type := |zz : nCk 0 0 | incl { m n : nat } : nCk m n -> nCk (S m) (S n) |