diff options
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 25 |
2 files changed, 26 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cc09170107..7f18065fe6 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -958,7 +958,7 @@ let interp_induction_arg ist gl arg = else let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in let f env sigma = - let (sigma,c) = interp_constr ist env sigma c in + let (sigma,c) = interp_open_constr ist env sigma c in sigma,(c,NoBindings) in keep,ElimOnConstr f diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 4704a08e59..c6eff3eebe 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -252,3 +252,28 @@ destruct H. - exact I. - reflexivity. Qed. + +(* Check destruct on idents with maximal implicit arguments - which did + not work in 8.4 *) + +Parameter f : forall {n:nat}, n=n -> nat. +Goal f (eq_refl 0) = 0. +destruct f. +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. +intros. +destruct (f _). +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. +intros. +destruct f. |