diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 64edcd2e3..ded85464e 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -21,6 +21,7 @@ val new_sort_in_family : sorts_family -> sorts val new_Type : unit -> types val new_Type_sort : unit -> sorts val refresh_universes : types -> types +val refresh_universes_strict : types -> types (* printers *) val print_sort : sorts -> std_ppcmds |