Avoid computing tactic printing tree (std_ppcmds) when printing not needed in

eauto and class_tactics

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

2 files changed, 12 insertions, 12 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index ba83fb5a8..f1cea877a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -188,8 +188,8 @@ and e_my_find_search db_list local_db hdc concl =
 	  | Extern tacast -> conclPattern concl p tacast
       in
 	match t with
-	| Extern _ -> (tac,b,true,pr_autotactic t)
-	| _ -> (tac,b,false,pr_autotactic t)
+	| Extern _ -> (tac,b,true,lazy (pr_autotactic t))
+	| _ -> (tac,b,false,lazy (pr_autotactic t))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db gl =
@@ -224,7 +224,7 @@ let typeclasses_debug = ref false
 let pr_depth l = prlist_with_sep (fun () -> str ".") pr_int (List.rev l)
 
 type autoinfo = { hints : Auto.hint_db; is_evar: existential_key option;
-		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds }
+		  only_classes: bool; auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t}
 type autogoal = goal * autoinfo
 type 'ans fk = unit -> 'ans
 type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
@@ -279,7 +279,7 @@ let intro_tac : atac =
 	  let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) 
 	    (true,false,false) info.only_classes None (List.hd context) in
 	  let ldb = Hint_db.add_list hint info.hints in
-	    (g', { info with is_evar = None; hints = ldb; auto_last_tac = str"intro" })) gls
+	    (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls
       in {it = gls'; sigma = s})
 
 let normevars_tac : atac = 
@@ -344,7 +344,7 @@ let hints_tac hints =
     let tacs = List.sort compare tacs in
     let rec aux i = function
       | (_, pp, b, {it = gls; sigma = s}) :: tl ->
-	  if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ pp
+	  if !typeclasses_debug then msgnl (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
 					       ++ str" on" ++ spc () ++ pr_ev s gl);
 	  let fk =
 	    (fun () -> (* if !typeclasses_debug then msgnl (str"backtracked after " ++ pp); *)
@@ -451,7 +451,7 @@ let rec fix (t : 'a tac) : 'a tac =
 let make_autogoal ?(only_classes=true) ?(st=full_transparent_state) ev g =
   let hints = make_autogoal_hints only_classes ~st g in
     (g.it, { hints = hints ; is_evar = ev; 
-	     only_classes = only_classes; auto_depth = []; auto_last_tac = mt() })
+	     only_classes = only_classes; auto_depth = []; auto_last_tac = lazy (mt()) })
       
 let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) gs evm' =
   { it = list_map_i (fun i g -> 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index ebef403a1..2d18c36fe 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -134,7 +134,7 @@ and e_my_find_search db_list local_db hdc concl =
 	   | Unfold_nth c -> h_reduce (Unfold [all_occurrences_expr,c]) onConcl
 	   | Extern tacast -> conclPattern concl p tacast
        in
-       (tac,pr_autotactic t))
+       (tac,lazy (pr_autotactic t)))
        (*i
 	 fun gls -> pPNL (pr_autotactic t); Format.print_flush ();
                      try tac gls
@@ -168,7 +168,7 @@ let find_first_goal gls =
 type search_state = {
   depth : int; (*r depth of search before failing *)
   tacres : goal list sigma;
-  last_tactic : std_ppcmds;
+  last_tactic : std_ppcmds Lazy.t;
   dblist : Auto.hint_db list;
   localdb :  Auto.hint_db list }
 
@@ -219,7 +219,7 @@ module SearchProblem = struct
 	  filter_tactics s.tacres
 	    (List.map
 	       (fun id -> (e_give_exact (mkVar id),
-			   (str "exact" ++ spc () ++ pr_id id)))
+			   lazy (str "exact" ++ spc () ++ pr_id id)))
 	       (pf_ids_of_hyps g))
 	in
 	List.map (fun (res,pp) -> { depth = s.depth; tacres = res;
@@ -237,7 +237,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,lazy (str "intro")])
       in
       let rec_tacs =
 	let l =
@@ -260,7 +260,7 @@ module SearchProblem = struct
 
   let pp s =
     msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++
-		  s.last_tactic ++ str "\n"))
+		  (Lazy.force s.last_tactic) ++ str "\n"))
 
 end
 
@@ -269,7 +269,7 @@ module Search = Explore.Make(SearchProblem)
 let make_initial_state n gl dblist localdb =
   { depth = n;
     tacres = tclIDTAC gl;
-    last_tactic = (mt ());
+    last_tactic = lazy (mt());
     dblist = dblist;
     localdb = [localdb] }