From ef2776e7de84cd324392f52fed2dfa72a44a97b1 Mon Sep 17 00:00:00 2001
From: gmelquio
Date: Thu, 28 Apr 2011 14:29:16 +0000
Subject: 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
---
 tactics/tacinterp.ml | 5 +++--
 1 file 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
-- 
cgit v1.2.3