X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=6fc9b2eee467bc9e15073e4cd3e94a0d354f0cef;hb=9d33fd0863f207cee7f882ae28c83e1944d2a0f1;hp=7c58ae87e5fca689fd807990ab6a45cdc0395055;hpb=806ecbdd749ecf2a1cabff52b41cf748fe022401;p=helm.git

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 7c58ae87e..6fc9b2eee 100644
--- a/helm/software/components/ng_tactics/nInversion.ml
+++ b/helm/software/components/ng_tactics/nInversion.ml
@@ -11,6 +11,9 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
+(*let pp m = prerr_endline (Lazy.force m);;*)
+let pp _ = ();;
+
 let fresh_name =
  let i = ref 0 in
  function () ->
@@ -69,30 +72,30 @@ let subst_metasenv_and_fix_names status =
 ;;
 
 let mk_inverter name it leftno ?selection outsort status baseuri =
- prerr_endline ("leftno = " ^ string_of_int leftno);
+ pp (lazy ("leftno = " ^ string_of_int leftno));
  let _,ind_name,ty,cl = it in
- prerr_endline ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty);
+ pp (lazy ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
  let ncons = List.length cl in
  (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
  let params = List.rev_map (function name,_ -> mk_id name) params in
- prerr_endline ("lunghezza params = " ^ string_of_int (List.length params));*)
+ pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));*)
  let args,sort= split_arity ~subst:[] [] ty in
- prerr_endline ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort);
+ pp (lazy ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort));
  (*let args = List.rev_map (function name,_ -> mk_id name) args in
- prerr_endline ("lunghezza args = " ^ string_of_int (List.length args));*)
+ pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));*)
  let nparams = List.length args in
- prerr_endline ("nparams = " ^ string_of_int nparams);
+ pp (lazy ("nparams = " ^ string_of_int nparams));
  if nparams <= leftno 
    then raise (Failure "inverter: the type must have at least one right parameter") 
    else 
      let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in
-     prerr_endline ("lunghezza xs = " ^ string_of_int (List.length xs));
+     pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs)));
      let ls, rs = HExtlib.split_nth leftno xs in
-     prerr_endline ("lunghezza ls = " ^ string_of_int (List.length ls));
-     prerr_endline ("lunghezza rs = " ^ string_of_int (List.length rs));
+     pp (lazy ("lunghezza ls = " ^ string_of_int (List.length ls)));
+     pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs)));
      let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in
     
-     let id_xs = List.map mk_id xs in
+     let _id_xs = List.map mk_id xs in
      let id_ls = List.map mk_id ls in
      let id_rs = List.map mk_id rs in
      let id_ys = List.map mk_id ys in
@@ -117,7 +120,7 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
          | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1)
        in (hypaux 1 ncons)
      in
-     prerr_endline ("lunghezza ys = " ^ string_of_int (List.length ys));
+     pp (lazy ("lunghezza ys = " ^ string_of_int (List.length ys)));
     
      let outsort, suffix = NCicElim.ast_of_sort outsort in
      let theorem = mk_prods xs