Backtrack du commit de Christine, qui posait probleme avec FTC

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3842 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 17 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d058ad543b..02c0e65918 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -753,23 +753,13 @@ let exact_proof c gl =
 
 let (assumption : tactic) = fun gl ->
   let concl =  pf_concl gl in 
-  if occur_existential concl then 
-    let rec arec = function
-      | [] -> error "No such assumption"
-      | (id,_,t)::rest -> 
-	  (try tclTHEN (unify t) (exact_check (mkVar id)) gl
-	   with UserError _ | Logic.RefinerError _ ->  arec rest)
-    in
-      arec (pf_hyps gl)
-  else
-    let rec arec = function
-      | [] -> error "No such assumption"
-      | (id,_,t)::rest -> 
-	  if pf_conv_x_leq gl t concl then refine_no_check (mkVar id) gl
-	  else arec rest
-    in
-      arec (pf_hyps gl)
-
+  let rec arec = function
+    | [] -> error "No such assumption"
+    | (id,c,t)::rest -> 
+	if pf_conv_x_leq gl t concl then refine_no_check (mkVar id) gl
+	else arec rest
+  in
+  arec (pf_hyps gl)
 
 (*****************************************************************)
 (*          Modification of a local context                      *)