From 6b0b6d841363d4a1b195b0a9283d596736bf8bbf Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Thu, 28 Apr 2011 14:33:40 +0000
Subject: 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
---
 tactics/tacinterp.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 65621a0288..3012cbae2f 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
-- 
cgit v1.2.3