Prise en compte des notations "alias" dans la globalisation des coercions.

Au passage, un peu plus de standardisation des noms de fonctions de
globalisation 

Principe de base :

  locate_foo : qualid -> foo                   (échoue avec Not_found)
  global : reference -> global_reference       (échoue avec UserError)
  global_of_foo : foo -> global_reference      (échoue avec UserError)

  f_with_alias : se comporte comme f mais prenant aussi en compte les
    notations de la forme "Notation id:=ref"

Principale exception :

  locate, au lieu de locate_global
  locate_global_with_alias, qui prend en entrée un "qualid located"

Restent beaucoup de fonctions qui pourraient utiliser
global_with_alias au lieu de global, notamment dans contribs.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 5 deletions

diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 50f2f3e7d7..e83cb8885f 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,6 +13,7 @@ open Util
 open Names
 open Topconstr
 open Rawterm
+open Libnames
 (*i*)
 
 (* Syntactic definitions. *)
@@ -23,10 +24,16 @@ val declare_syntactic_definition : bool -> identifier -> bool -> aconstr
 val search_syntactic_definition : loc -> kernel_name -> rawconstr
 
 
-(* [locate_global] locates global reference possibly following a chain of 
-   syntactic aliases; 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 *)
+(* [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 : Libnames.qualid -> Libnames.global_reference
+val locate_global_with_alias : qualid located -> global_reference
+
+(* Locate a reference taking into account possible "alias" notations *)
+val global_with_alias : reference -> global_reference
+
+(* The same for inductive types *)
+val inductive_of_reference_with_alias : reference -> inductive