diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-27 08:44:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-27 09:57:11 +0100 |
| commit | 4249ab5cac5bb0d638400b14c389ded98b3c8ea8 (patch) | |
| tree | 8767aab68245c09b04c4499cbf6260ce0b461769 /tactics | |
| parent | 47828f078ac7359e8e2e1891bc6ef48812bb73a5 (diff) | |
Making destruct on idents with maximal implicit arguments working, by
keeping them as open holes. When these arguments are class instances,
this restores compatibility with the 8.4 search for subterms from
non-fully applied patterns which was using conversion on the
instances.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cc0917010..7f18065fe 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 |