X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=4b4b7246d29023962c35dddc3e8dfc2b6a05b72b;hb=6c3b2a89bd14bb8a96e56565b725dd635effc2e5;hp=89a1dd1af65b33bdb126e68575e79358c72d12d6;hpb=870b9b017da98021d9163bf45efe9c27b40bb33d;p=helm.git

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 89a1dd1af..4b4b7246d 100644
--- a/helm/software/components/ng_tactics/nInversion.ml
+++ b/helm/software/components/ng_tactics/nInversion.ml
@@ -11,8 +11,8 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-let pp m = prerr_endline (Lazy.force m);;
-(* let pp _ = ();; *)
+(* let pp m = prerr_endline (Lazy.force m);;*)
+let pp _ = ();;
 
 let fresh_name =
  let i = ref 0 in
@@ -130,11 +130,9 @@ let mk_inverter name it leftno ?selection outsort status baseuri =
                                       Some (CicNotationPt.Implicit `JustOne)),
                                       mk_appl (mk_id "P"::id_rs)))))
      in
-     pp (lazy ("and the theorem is: \n" ^ (CicNotationPp.pp_term theorem))); 
      let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @
                        List.map mk_id hyplist @ 
                        HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys) @ [mk_id "Hterm"] ) in
-     pp (lazy ("and t is: \n" ^ (CicNotationPp.pp_term t))); 
      let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
                              (baseuri ^ name ^ ".def",
                                0,CicNotationPt.Theorem (`Theorem,name,theorem,Some