From 2509bd1c7ccc764e5a6fdb04a9943e875501818a Mon Sep 17 00:00:00 2001
From: filliatr
Date: Thu, 1 Feb 2001 08:49:40 +0000
Subject: oubli de Closure.EvalConstRef

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1305 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tauto.ml4 | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 0415bae4da..72874009f8 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -2049,14 +2049,16 @@ let rec prove  tauto_intu g   =
 			    (prove tauto_intu)))
    tauto_intu)))))))))) g
 
+let strToOccs x = 
+  ([], Closure.EvalConstRef (Nametab.constant_sp_of_id (id_of_string x)))
+
 let tauto gls = 
-  let strToOccs x = ([],Nametab.constant_sp_of_id (id_of_string x)) in  
-  (tclTHEN (onAllClausesLR 
-              (unfold_option [strToOccs "not";strToOccs "iff"])) 
+  (tclTHEN 
+     (onAllClausesLR 
+        (unfold_option [strToOccs "not";strToOccs "iff"])) 
      (prove tautoOR_0)) gls
 
 let intuition gls =
-  let strToOccs x = ([],Nametab.constant_sp_of_id (id_of_string x)) in  
   (tclTHEN 
      ((tclTHEN (onAllClausesLR 
 		  (unfold_option [strToOccs "not";strToOccs "iff"])) 
-- 
cgit v1.2.3