diff options
| author |  gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-28 14:33:40 +0000 |
|---|---|---|
| committer | gmelquio <gmelquio@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-28 14:33:40 +0000 |
| commit | 6b0b6d841363d4a1b195b0a9283d596736bf8bbf (patch) | |
| tree | 45ac7fcd7ae7a24ba861371586107df42056344d | |
| parent | ef2776e7de84cd324392f52fed2dfa72a44a97b1 (diff) | |
Revert r14078 "Partial backtrack on the support for open terms in destruct/induction:"
While this is needed for supporting destruct with typeclasses on 8.4, it was not my intent to commit it yet (as a better fix might be in the work), so reverting it for now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14079 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 65621a028..3012cbae2 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1570,9 +1570,8 @@ let interp_induction_arg ist gl sigma arg = let env = pf_env gl in match arg with | 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) + let sigma, c = interp_constr_with_bindings ist env sigma c in + sigma, ElimOnConstr c | ElimOnAnonHyp n as x -> sigma, x | ElimOnIdent (loc,id) -> try |