Réparation d'une inefficacité bêtement introduite dans la révision

10222: n'évaluer les std_ppcmds que si vraiment ils sont utilisés (en
particulier, les [< ... >] sont paresseux comme on l'attend mais pas
les ++).



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

1 files changed, 27 insertions, 27 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 71039e3bb8..abe06e5d3a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1061,15 +1061,15 @@ let get_debug () = !debug
 let debugging_step ist pp =
   match ist.debug with
   | DebugOn lev ->
-      safe_msgnl (str "Level " ++ int lev ++ str": " ++ pp ++ fnl())
+      safe_msgnl (str "Level " ++ int lev ++ str": " ++ pp () ++ fnl())
   | _ -> ()
 
 let debugging_exception_step ist signal_anomaly e pp =
   let explain_exc =
     if signal_anomaly then explain_logic_error
     else explain_logic_error_no_anomaly in
-  debugging_step ist 
-    (pp ++ spc() ++ str "raised the exception" ++ fnl() ++ !explain_exc e)
+  debugging_step ist (fun () -> 
+    pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ !explain_exc e)
 
 let error_ltac_variable loc id env v s =
    user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++ 
@@ -1463,8 +1463,8 @@ let interp_may_eval f ist gl = function
      try 
 	f ist gl c
      with e ->
-       debugging_exception_step ist false e
-         (str"interpretation of term " ++ pr_rawconstr_env (pf_env gl)(fst c));
+       debugging_exception_step ist false e (fun () ->
+         str"interpretation of term " ++ pr_rawconstr_env (pf_env gl) (fst c));
        raise e  
 
 (* Interprets a constr expression possibly to first evaluate *)
@@ -1473,7 +1473,7 @@ let interp_constr_may_eval ist gl c =
     try
       interp_may_eval pf_interp_constr ist gl c
     with e ->
-      debugging_exception_step ist false e (str "evaluation of term");
+      debugging_exception_step ist false e (fun () -> str"evaluation of term");
       raise e
   in
   begin
@@ -1686,10 +1686,10 @@ and interp_app ist gl fv largs loc =
             let lloc = if lval=[] then loc else ist.last_loc in
 	    val_interp { ist with lfun=newlfun@olfun; last_loc=lloc } gl body
 	  with e ->
-            debugging_exception_step ist false e (str "evaluation");
+            debugging_exception_step ist false e (fun () -> str "evaluation");
 	    raise e in
-        debugging_step ist 
-	  (str "evaluation returns" ++ fnl() ++ pr_value (Some (pf_env gl)) v);
+        debugging_step ist (fun () ->
+	  str "evaluation returns" ++ fnl() ++ pr_value (Some (pf_env gl)) v);
         if lval=[] then v else interp_app ist gl v lval loc
       else
         VFun(newlfun@olfun,lvar,body)
@@ -1942,20 +1942,20 @@ and interp_match ist g lz constr lmr =
             let lm = 
               try matches c csr
               with e ->
-                debugging_exception_step ist false e
-                  (str "matching with pattern" ++ fnl () ++
-                   pr_constr_pattern_env (pf_env g) c);
+                debugging_exception_step ist false e (fun () ->
+                  str "matching with pattern" ++ fnl () ++
+                  pr_constr_pattern_env (pf_env g) c);
                 raise e in
             try
               let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
               eval_with_fail { ist with lfun=lm@ist.lfun } lz g mt
             with e ->
-              debugging_exception_step ist false e
-                (str "rule body for pattern" ++
-                 pr_constr_pattern_env (pf_env g) c);
+              debugging_exception_step ist false e (fun () ->
+                str "rule body for pattern" ++
+                pr_constr_pattern_env (pf_env g) c);
               raise e
          with e when is_match_catchable e ->
-           debugging_step ist (str "switching to the next rule");
+           debugging_step ist (fun () -> str "switching to the next rule");
            apply_match ist csr tl)
 
     | (Pat ([],Subterm (id,c),mt))::tl ->
@@ -1967,31 +1967,31 @@ and interp_match ist g lz constr lmr =
   let csr = 
       try interp_ltac_constr ist g constr with e ->
         debugging_exception_step ist true e
-          (str "evaluation of the matched expression");
+          (fun () -> str "evaluation of the matched expression");
         raise e in
   let ilr = read_match_rule (fst (constr_list ist (pf_env g))) lmr in
   let res = 
      try apply_match ist csr ilr with e -> 
-       debugging_exception_step ist true e (str "match expression");
+       debugging_exception_step ist true e (fun () -> str "match expression");
        raise e in
-  debugging_step ist 
-    (str "match expression returns " ++ pr_value (Some (pf_env g)) res);
+  debugging_step ist (fun () ->
+    str "match expression returns " ++ pr_value (Some (pf_env g)) res);
   res
 
 (* Interprets tactic expressions : returns a "constr" *)
 and interp_ltac_constr ist gl e =
   let result = 
   try val_interp ist gl e with Not_found -> 
-    debugging_step ist 
-      (str "evaluation failed for" ++ fnl() ++
-       Pptactic.pr_glob_tactic (pf_env gl) e);
+    debugging_step ist (fun () ->
+      str "evaluation failed for" ++ fnl() ++
+      Pptactic.pr_glob_tactic (pf_env gl) e);
     raise Not_found in
   try
     let cresult = constr_of_value (pf_env gl) result in
-    debugging_step ist
-      (Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
-       str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult);
-     cresult
+    debugging_step ist (fun () ->
+      Pptactic.pr_glob_tactic (pf_env gl) e ++ fnl() ++
+      str " has value " ++ fnl() ++ print_constr_env (pf_env gl) cresult);
+    cresult
   with Not_found ->
     errorlabstrm ""
       (str "Must evaluate to a term" ++ fnl() ++