diff options
| author | barras | 2004-09-15 16:50:56 +0000 |
|---|---|---|
| committer | barras | 2004-09-15 16:50:56 +0000 |
| commit | 2d707f4445c0cc86d8f8c30bdbe9eecf956997f9 (patch) | |
| tree | 9d6c2ff5489ba6bbf5683963108c34aa10b81e6f /pretyping/termops.mli | |
| parent | 8f5a7bbf2e5c64d6badd9e7c39da83d07b9c6f40 (diff) | |
hiding the meta_map in evar_defs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 8ce7b39dcb..e1a9d5ba95 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -19,6 +19,9 @@ open Environ (*val set_module : Names.dir_path -> unit*) val new_univ : unit -> Univ.universe val new_sort_in_family : sorts_family -> sorts +val new_Type : unit -> types +val new_Type_sort : unit -> sorts +val refresh_universes : types -> types (* printers *) val print_sort : sorts -> std_ppcmds |