diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
| commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
| tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /test-suite/bugs/closed/2016.v | |
| parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) | |
Imported Upstream version 8.6
Diffstat (limited to 'test-suite/bugs/closed/2016.v')
| -rw-r--r-- | test-suite/bugs/closed/2016.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/2016.v b/test-suite/bugs/closed/2016.v index 13ec5bea..536e6fab 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. |