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