From 6da130f2ed2b8a66e7987198378cb81890c4ae03 Mon Sep 17 00:00:00 2001
From: mohring
Date: Tue, 6 Mar 2001 13:48:09 +0000
Subject: Modification de e_give_exact pour eviter d'echouer sur l'unification
 en l'absence de variables existentielles

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1431 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/eauto.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 26467421fc..9ab7ec5d64 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -15,7 +15,10 @@ open Pattern
 open Clenv
 open Auto
 
-let e_give_exact c gl = tclTHEN (unify (pf_type_of gl c)) (exact_no_check c) gl
+let e_give_exact c gl = let t1 = (pf_type_of gl c) and t2 = pf_concl gl in 
+  if occur_existential t1 or occur_existential t2 then 
+     tclTHEN (unify t1) (exact_no_check c) gl
+  else exact_no_check c gl
 
 let assumption id = e_give_exact (mkVar id)
         
-- 
cgit v1.2.3