diff options
Diffstat (limited to 'interp/syntax_def.mli')
| -rw-r--r-- | interp/syntax_def.mli | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index fb0c3c9f2..3ba78e91d 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -25,19 +25,3 @@ val declare_syntactic_definition : bool -> identifier -> bool -> syndef_interpretation -> unit val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation - -(* [locate_global_with_alias] locates global reference possibly following - a notation if this notation has a role of aliasing; raise Not_found - if not bound in the global env; raise an error if bound to a - syntactic def that does not denote a reference *) - -val locate_global_with_alias : qualid located -> global_reference - -(* Extract a global_reference from a reference that can be an "alias" *) -val global_of_extended_global : extended_global_reference -> global_reference - -(* Locate a reference taking into account possible "alias" notations *) -val global_with_alias : reference -> global_reference - -(* The same for inductive types *) -val global_inductive_with_alias : reference -> inductive |