diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/destruct.v | 41 |
1 files changed, 21 insertions, 20 deletions
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 5f94d8e72..f1aebf6cc 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -263,20 +263,21 @@ Abort. (* This one was working in 8.4 (because of full conv on closed arguments) *) -Class A. -Instance a:A. -Goal forall f : A -> nat -> nat, f (id a) 0 = f a 0. +Class E. +Instance a:E. +Goal forall h : E -> nat -> nat, h (id a) 0 = h a 0. intros. -destruct (f _). +destruct (h _). change (0=0). Abort. (* This one was not working in 8.4 because an occurrence of f was remaining, blocking the "clear f" *) -Goal forall f : A -> nat -> nat, f a 0 = f a 1. +Goal forall h : E -> nat -> nat, h a 0 = h a 1. intros. -destruct f. +destruct h. +Abort. (* This was not working in 8.4 *) @@ -292,30 +293,30 @@ End S1. (* This was not working in 8.4 *) -Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. +Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. intros. -induction g. -2:change (n = g 1 -> n = g 2) in IHn. +induction h. +2:change (n = h 1 -> n = h 2) in IHn. Abort. (* This was not working in 8.4 *) -Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. -intros g H H0. -induction g in H |- *. +Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. +intros h H H0. +induction h in H |- *. Abort. (* "at" was not granted in 8.4 in the next two examples *) -Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. -intros g H H0. -induction g in H at 2, H0 at 1. -change (g 0 = 0) in H. +Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. +intros h H H0. +induction h in H at 2, H0 at 1. +change (h 0 = 0) in H. Abort. -Goal forall g:nat->nat, g 0 = g 1 -> g 1 = g 2 -> g 0 = g 2. -intros g H H0. -Fail induction g in H at 2 |- *. (* Incompatible occurrences *) +Goal forall h:nat->nat, h 0 = h 1 -> h 1 = h 2 -> h 0 = h 2. +intros h H H0. +Fail induction h in H at 2 |- *. (* Incompatible occurrences *) Abort. (* These ones are not satisfactory at the current time @@ -329,7 +330,6 @@ destruct H. H : n = n ============================ 0 = n -*) Abort. End S2. @@ -353,3 +353,4 @@ destruct H. ============================ x0=1 *) +*) |