From 8e328c6c3b2d6cfe3110abdfe5bb57eeba9c0cc4 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 14 Jul 2014 12:44:32 +0200 Subject: 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. --- interp/smartlocate.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'interp/smartlocate.mli') 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 -- cgit v1.2.3