(* $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
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