diff options
| author | gmelquio | 2011-04-28 14:29:16 +0000 |
|---|---|---|
| committer | gmelquio | 2011-04-28 14:29:16 +0000 |
| commit | ef2776e7de84cd324392f52fed2dfa72a44a97b1 (patch) | |
| tree | 2e7cc19dbc082477c042dd1b8d7f4ad7210815b6 | |
| parent | f5276a11a40f86d5ed8ff14bd03d6ea71e7dad33 (diff) | |
Partial backtrack on the support for open terms in destruct/induction:
use type classes to possibly solve evars before trying to unify the
term (or the dependencies of its type) agains a subterm of the current
goal. This solves compatibility bug #2222. Mixing unification and type
classes is left for future work.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14078 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 3012cbae2f..65621a0288 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1570,8 +1570,9 @@ let interp_induction_arg ist gl sigma arg = let env = pf_env gl in match arg with | ElimOnConstr c -> - let sigma, c = interp_constr_with_bindings ist env sigma c in - sigma, ElimOnConstr c + let sigma', (c,b) = interp_constr_with_bindings ist env sigma c in + let sigma, c = solve_remaining_evars false true env sigma sigma' c in + sigma, ElimOnConstr (c,b) | ElimOnAnonHyp n as x -> sigma, x | ElimOnIdent (loc,id) -> try |