From e23f78a6e50cb2ebf1e182ff66f0ca8f6f802ed3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 5 Feb 2006 22:56:16 +0000
Subject: Debugging en syntaxe v8

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

diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index fd1f38786a..bea6f33037 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -283,7 +283,7 @@ module SearchProblem = struct
 	  filter_tactics s.tacres
 	    (List.map 
 	       (fun id -> (e_give_exact_constr (mkVar id),
-			   (str "Exact" ++ spc () ++ pr_id id)))
+			   (str "exact" ++ spc () ++ pr_id id)))
 	       (pf_ids_of_hyps g))
 	in
 	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
@@ -301,7 +301,7 @@ module SearchProblem = struct
 	     { depth = s.depth; tacres = res; 
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb })
-	  (filter_tactics s.tacres [Tactics.intro,(str "Intro")])
+	  (filter_tactics s.tacres [Tactics.intro,(str "intro")])
       in
       let rec_tacs = 
 	let l = 
-- 
cgit v1.2.3