Disabled debug prints in ndestruct tactic.

diff --git a/helm/software/components/ng_tactics/nDestructTac.ml b/helm/software/components/ng_tactics/nDestructTac.ml
index 01ca13ee1f931a91e2f0be628fdab39f35b550c7..b2faf6d9627df7cb219902797062fc17da946925 100644 (file)
--- a/helm/software/components/ng_tactics/nDestructTac.ml
+++ b/helm/software/components/ng_tactics/nDestructTac.ml
@@ -28,7 +28,7 @@
 open NTacStatus
 open Continuationals.Stack
 
-let debug = true 
+let debug = false 
 let pp = 
   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
 
@@ -74,7 +74,6 @@ let subst_metasenv_and_fix_names status =
 (* input: nome della variabile riscritta
  * output: lista dei nomi delle variabili il cui tipo dipende dall'input *)
 let cascade_select_in_ctx ~subst ctx iname =
-  prerr_endline "C";
   let lctx, rctx = HExtlib.split_nth (iname - 1) ctx in
   let lctx = List.rev lctx in
   let rec rm_last = function
@@ -84,22 +83,18 @@ let cascade_select_in_ctx ~subst ctx iname =
 
   let indices,_ = List.fold_left
        (fun (acc,context) item -> 
-         prerr_endline "C2";
           match item with
             | n,(NCic.Decl s | NCic.Def (s,_)) 
                   when not (List.for_all (fun x -> NCicTypeChecker.does_not_occur ~subst context (x-1) x s) acc) ->
-                List.iter (fun m -> prerr_endline ("acc has " ^ (string_of_int m))) acc;
-                prerr_endline ("acc occurs in the type of " ^ n);
+                List.iter (fun m -> pp (lazy ("acc has " ^ (string_of_int m)))) acc;
+                pp (lazy ("acc occurs in the type of " ^ n));
                 (1::List.map ((+) 1) acc, item::context)
             | _ -> (List.map ((+) 1) acc, item::context))
        ([1], rctx) lctx in
-    prerr_endline "C3:";
-    List.iter (fun n -> prerr_endline (string_of_int n)) indices;
     let indices = rm_last indices in
     let res = List.map (fun n -> let s,_ = List.nth ctx (n-1) in s) indices in
-    prerr_endline "C4:";
-    List.iter (fun n -> prerr_endline n) res;
-    prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst ctx);
+    List.iter (fun n -> pp (lazy n)) res;
+    pp (lazy (NCicPp.ppcontext ~metasenv:[] ~subst ctx));
     res, indices
 ;;
 
@@ -123,7 +118,7 @@ let arg_list nleft t =
 ;;
 
 let nargs it nleft consno =
-  prerr_endline (Printf.sprintf "nargs %d %d" nleft consno);
+  pp (lazy (Printf.sprintf "nargs %d %d" nleft consno));
   let _,indname,_,cl = it in
   let _,_,t_k = List.nth cl consno in
   List.length (arg_list nleft t_k) ;;
@@ -266,10 +261,10 @@ let discriminate_tac ~context cur_eq status =
   pp (lazy (Printf.sprintf "discriminate: equation %s" (name_of_rel ~context cur_eq)));
 
   let dbranch it leftno consno =
-    prerr_endline (Printf.sprintf "dbranch %d %d" leftno consno);
+    pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
     let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
     (* (\forall ...\forall P.\forall DH : ( ... = ... -> P). P) *)
-    let params = List.map (fun x -> prerr_endline (Printf.sprintf "dbranch param a%d" x); NTactics.intro_tac ("a" ^ string_of_int x)) nlist in
+    let params = List.map (fun x -> NTactics.intro_tac ("a" ^ string_of_int x)) nlist in
         NTactics.reduce_tac ~reduction:(`Normalize true) ~where:default_pattern::
         params @ [
         NTactics.intro_tac "P";
@@ -278,21 +273,18 @@ let discriminate_tac ~context cur_eq status =
         NTactics.apply_tac ("",0,mk_id "refl");
     ] in
   let dbranches it leftno =
-    prerr_endline (Printf.sprintf "dbranches %d" leftno);
+    pp (lazy (Printf.sprintf "dbranches %d" leftno));
     let _,_,_,cl = it in
     let nbranches = List.length cl in 
     let branches = iter (fun n acc -> 
       let m = nbranches - n - 1 in
-      if m = 0 then (prerr_endline "no shift"; acc @ (dbranch it leftno m))
-      else (prerr_endline "sì shift"; acc @ NTactics.shift_tac :: (dbranch it
-      leftno m)))
+      if m = 0 then acc @ (dbranch it leftno m)
+      else acc @ NTactics.shift_tac :: (dbranch it
+      leftno m))
       (nbranches-1) [] in
     if nbranches > 1 then
-      (prerr_endline "sì branch";
-         NTactics.branch_tac:: branches @ [NTactics.merge_tac])
-    else
-      (prerr_endline "no branch";
-      branches)
+         NTactics.branch_tac:: branches @ [NTactics.merge_tac]
+    else branches
   in
   
   let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
@@ -311,8 +303,8 @@ let discriminate_tac ~context cur_eq status =
       | NCic.Appl (NCic.Const 
           (NReference.Ref (uri, NReference.Ind (_,indtyno,_)) as r)::_) -> 
         uri, indtyno, NCicEnvironment.get_checked_indtys r
-      | _ -> prerr_endline ("discriminate: indty ="  ^ NCicPp.ppterm
-                  ~metasenv:[] ~subst:[] ~context:[] it) ; assert false in
+      | _ -> pp (lazy ("discriminate: indty ="  ^ NCicPp.ppterm
+                  ~metasenv:[] ~subst:[] ~context:[] it)) ; assert false in
     let _,leftno,its,_,_ = its in
     status, leftno, List.nth its indtyno
   in