ppterm ~formatter ~context ~subst ~metasenv ?inside_fix t
;;
-let rec ppcontext ~formatter ?(sep=";") ~subst ~metasenv = function
+let rec ppcontext ~formatter ?(sep="; ") ~subst ~metasenv = function
| [] -> ()
| (name, NCic.Decl t) :: tl ->
ppcontext ~formatter ~sep ~subst ~metasenv tl;
String.concat ","
(List.map
(function
- `IsSort -> "sort"
+ | `IsTerm -> "term"
+ | `IsType -> "type"
+ | `IsSort -> "sort"
| `Name n -> "name=" ^ n
| `InScope -> "in_scope"
| `OutScope n -> "out_scope:" ^ string_of_int n
ppsubst ~formatter ~subst ~metasenv tl
;;
-let ppsubst ~formatter ~metasenv subst =
- ppsubst ~formatter ~metasenv ~subst subst
+let ppsubst ~formatter ~metasenv ?(use_subst=true) subst =
+ let ssubst = if use_subst then subst else [] in
+ ppsubst ~formatter ~metasenv ~subst:ssubst subst
;;
let string_of_generated = function
let ppmetasenv ~subst metasenv = on_buffer (ppmetasenv ~subst) metasenv;;
-let ppsubst ~metasenv subst = on_buffer (ppsubst ~metasenv) subst;;
+let ppsubst ~metasenv ?use_subst subst =
+ on_buffer (ppsubst ~metasenv ?use_subst) subst
+;;
let ppobj obj = on_buffer ppobj obj;;