diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 97e8f68cc5..e861ebbe43 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -20,9 +20,13 @@ open Sign let print_sort = function | Prop Pos -> (str "Set") | Prop Null -> (str "Prop") -(* | Type _ -> (str "Type") *) | Type u -> (str "Type(" ++ Univ.pr_uni u ++ str ")") +let print_sort_family = function + | InSet -> (str "Set") + | InProp -> (str "Prop") + | InType -> (str "Type") + let current_module = ref empty_dirpath let set_module m = current_module := m |