Added syntax for ninversion tactic (still experimental).

[helm.git] / helm / software / components / ng_tactics / nInversion.ml

diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml
index 89a1dd1af65b33bdb126e68575e79358c72d12d6..4b4b7246d29023962c35dddc3e8dfc2b6a05b72b 100644 (file)
--- 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