diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-14 12:44:32 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-07-14 12:48:33 +0200 |
| commit | 8e328c6c3b2d6cfe3110abdfe5bb57eeba9c0cc4 (patch) | |
| tree | 03e9e4c6cdc662b66b7f97670af051793869e765 /interp/smartlocate.mli | |
| parent | 99cee0e8d64567c6a89ab665c6e4dfd934674142 (diff) | |
smartlocate: look for the head symbol for real
This bug was hacked around in ssreflect, but with the new idea
that parsing and interpretation are done in distinct phases the
work around could not be implemented anymore.
Diffstat (limited to 'interp/smartlocate.mli')
| -rw-r--r-- | interp/smartlocate.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 86aa69681..9006e3687 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -17,7 +17,7 @@ open Misctypes if not bound in the global env; raise a [UserError] if bound to a syntactic def that does not denote a reference *) -val locate_global_with_alias : qualid located -> global_reference +val locate_global_with_alias : ?head:bool -> 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 @@ -26,13 +26,13 @@ val global_of_extended_global : extended_global_reference -> global_reference May raise [Nametab.GlobalizationError _] for an unknown reference, or a [UserError] if bound to a syntactic def that does not denote a reference. *) -val global_with_alias : reference -> global_reference +val global_with_alias : ?head:bool -> reference -> global_reference (** The same for inductive types *) val global_inductive_with_alias : reference -> inductive (** Locate a reference taking into account notations and "aliases" *) -val smart_global : reference or_by_notation -> global_reference +val smart_global : ?head:bool -> reference or_by_notation -> global_reference (** The same for inductive types *) val smart_global_inductive : reference or_by_notation -> inductive |