diff options
Diffstat (limited to 'library/global.mli')
| -rw-r--r-- | library/global.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/global.mli b/library/global.mli index b51ce3c774..4a993d1aaa 100644 --- a/library/global.mli +++ b/library/global.mli @@ -48,7 +48,7 @@ val import : compiled_env -> unit (*s Some functions of [Environ] instanciated on the global environment. *) -val id_of_global : sorts oper -> identifier +val id_of_global : global_reference -> identifier (*s Re-exported functions of [Inductive], composed with [lookup_mind_specif]. *) |