notations <>, Assumption avec existentiel, replace term

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

1 files changed, 17 insertions, 7 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 02c0e6591..d058ad543 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -753,13 +753,23 @@ let exact_proof c gl =
 
 let (assumption : tactic) = fun gl ->
   let concl =  pf_concl gl in 
-  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)
+  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)
+
 
 (*****************************************************************)
 (*          Modification of a local context                      *)