Debugging code commented out.

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 7c58ae87e5fca689fd807990ab6a45cdc0395055..1ee47c74e97998dbfd552416ad7b12aec0589411 100644 (file)
--- 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 $ *)
 
 
 (* $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 () ->
 let fresh_name =
  let i = ref 0 in
  function () ->


@@ -69,27 +72,27 @@ let subst_metasenv_and_fix_names status =
 ;;
 
 let mk_inverter name it leftno ?selection outsort status baseuri =
 ;;
 
 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
  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
  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
  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
  (*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
  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
  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
      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 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


@@ -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
          | 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
     
      let outsort, suffix = NCicElim.ast_of_sort outsort in
      let theorem = mk_prods xs