F.fprintf f "@; @[<v>[ ";
if pl <> [] then
begin
- F.fprintf f "@[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor 1 r));
+ F.fprintf f "@[<hov 2>%s ⇒@;"
+ (try r2s inside_fix (R.mk_constructor 1 r)
+ with R.IllFormedReference _ -> "#ERROR#");
aux ~toplevel:true ctx (List.hd pl);
F.fprintf f "@]";
ignore(List.fold_left
(fun i t ->
- F.fprintf f "@;| @[<hov 2>%s ⇒@;" (r2s inside_fix (R.mk_constructor i r));
+ F.fprintf f "@;| @[<hov 2>%s ⇒@;"
+ (try r2s inside_fix (R.mk_constructor i r)
+ with R.IllFormedReference _ -> "#ERROR#");
aux ~toplevel:true ctx t;
F.fprintf f "@]";
i+1)
2 (List.tl pl));
end;
F.fprintf f "]@] @]";
+ | C.Appl [] | C.Appl [_] | C.Appl (C.Appl _::_) ->
+ F.fprintf f "BAD APPLICATION"
| C.Appl l ->
F.fprintf f "@[<hov 2>";
if not toplevel then F.fprintf f "(";
Buffer.contents buff
;;
+let ppterm ~context ~subst ~metasenv ?(margin=80) ?inside_fix t =
+ Format.set_margin margin;
+ ppterm ~context ~subst ~metasenv ?inside_fix t
+;;
+
+
let ppobj = function
| (u,_,metasenv,subst,NCic.Fixpoint (b, fl, _)) ->
"{"^NUri.string_of_uri u^"}\n"^
let ppsubst ~metasenv subst = ppsubst ~metasenv ~subst subst;;
-let _ = NCicSubstitution.set_ppterm ppterm;;
+let _ = NCicSubstitution.set_ppterm (ppterm ~margin:80);;