Renaming ETName and ETReference so as to fit the user-visible terminology.

ETName -> ETIdent
ETReference -> ETGlobal

5 files changed, 20 insertions, 20 deletions

diff --git a/parsing/extend.ml b/parsing/extend.ml
index a3e27f9cf5..6fe2956643 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -34,8 +34,8 @@ type production_level =
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
 type 'a constr_entry_key_gen =
-  | ETName
-  | ETReference
+  | ETIdent
+  | ETGlobal
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of Constrexpr.notation_entry * Notation_term.constr_as_binder_kind option * 'a
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
index 125ea01681..c36b3b17bf 100644
--- a/parsing/notgram_ops.ml
+++ b/parsing/notgram_ops.ml
@@ -49,14 +49,14 @@ let production_level_eq l1 l2 = match (l1,l2) with
 | (NextLevel | NumLevel _), _ -> false
 
 let constr_entry_key_eq eq v1 v2 = match v1, v2 with
-| ETName, ETName -> true
-| ETReference, ETReference -> true
+| ETIdent, ETIdent -> true
+| ETGlobal, ETGlobal -> true
 | ETBigint, ETBigint -> true
 | ETBinder b1, ETBinder b2 -> b1 == b2
 | ETConstr (s1,bko1,lev1), ETConstr (s2,bko2,lev2) ->
    notation_entry_eq s1 s2 && eq lev1 lev2 && Option.equal (=) bko1 bko2
 | ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
+| (ETIdent | ETGlobal | ETBigint | ETBinder _ | ETConstr _ | ETPattern _), _ -> false
 
 let level_eq_gen strict (s1, l1, t1, u1) (s2, l2, t2, u2) =
   let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 2e777d9602..b959f2afa9 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1183,7 +1183,7 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   syntax_extension_type:
-    [ [ IDENT "ident" -> { ETName } | IDENT "global" -> { ETReference }
+    [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
       | IDENT "bigint" -> { ETBigint }
       | IDENT "binder" -> { ETBinder true }
       | IDENT "constr" -> { ETConstr (InConstrEntry,None,None) }
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 9956c1546d..7c1a880c46 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -377,11 +377,11 @@ let unparsing_metavar i from typs =
   let x = List.nth typs (i-1) in
   let prec = snd (precedence_of_entry_type from x) in
   match x with
-  | ETConstr _ | ETReference | ETBigint ->
+  | ETConstr _ | ETGlobal | ETBigint ->
      UnpMetaVar (i,prec)
   | ETPattern _ ->
      UnpBinderMetaVar (i,prec)
-  | ETName ->
+  | ETIdent ->
      UnpBinderMetaVar (i,prec)
   | ETBinder isopen ->
      assert false
@@ -635,8 +635,8 @@ let include_possible_similar_trailing_pattern typ etyps sl l =
   try_aux 0 l
 
 let prod_entry_type = function
-  | ETName -> ETProdName
-  | ETReference -> ETProdReference
+  | ETIdent -> ETProdName
+  | ETGlobal -> ETProdReference
   | ETBigint -> ETProdBigint
   | ETBinder _ -> assert false (* See check_binder_type *)
   | ETConstr (s,_,p) -> ETProdConstr (s,p)
@@ -949,7 +949,7 @@ let set_entry_type from etyps (x,typ) =
       | ETConstr (s,bko,Some n), (_,InternalProd) ->
          ETConstr (s,bko,(n,InternalProd))
       | ETPattern (b,n), _ -> ETPattern (b,n)
-      | (ETName | ETBigint | ETReference | ETBinder _ as x), _ -> x
+      | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
       | ETConstr (s,bko,None), _ -> ETConstr (s,bko,typ)
     with Not_found ->
       ETConstr (from,None,typ)
@@ -972,8 +972,8 @@ let join_auxiliary_recursive_types recvars etyps =
 
 let internalization_type_of_entry_type = function
   | ETBinder _ -> NtnInternTypeOnlyBinder
-  | ETConstr _ | ETBigint | ETReference
-  | ETName | ETPattern _ -> NtnInternTypeAny
+  | ETConstr _ | ETBigint | ETGlobal
+  | ETIdent | ETPattern _ -> NtnInternTypeAny
 
 let set_internalization_type typs =
   List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -992,9 +992,9 @@ let make_interpretation_type isrec isonlybinding = function
   (* Parsed as constr, interpreted as constr *)
   | ETConstr (_,None,_) -> NtnTypeConstr
   (* Others *)
-  | ETName -> NtnTypeBinder NtnParsedAsIdent
+  | ETIdent -> NtnTypeBinder NtnParsedAsIdent
   | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
-  | ETBigint | ETReference -> NtnTypeConstr
+  | ETBigint | ETGlobal -> NtnTypeConstr
   | ETBinder _ ->
      if isrec then NtnTypeBinderList
      else anomaly Pp.(str "Type binder is only for use in recursive notations for binders.")
@@ -1067,8 +1067,8 @@ let is_coercion = function
          let subentry = subentry_of_constr_prod_entry e in
          if notation_entry_level_eq subentry customkey then None
          else Some (IsEntryCoercion subentry)
-     | ETReference, InCustomEntry s -> Some (IsEntryGlobal (s,n))
-     | ETName, InCustomEntry s -> Some (IsEntryIdent (s,n))
+     | ETGlobal, InCustomEntry s -> Some (IsEntryGlobal (s,n))
+     | ETIdent, InCustomEntry s -> Some (IsEntryIdent (s,n))
      | _ -> None)
   | Some _ -> assert false
   | None -> None
@@ -1110,7 +1110,7 @@ let find_precedence custom lev etyps symbols onlyprint =
           user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
       (try match List.assoc x etyps, custom with
         | ETConstr (s,_,Some _), s' when s = s' -> test ()
-        | (ETName | ETBigint | ETReference), _ ->
+        | (ETIdent | ETBigint | ETGlobal), _ ->
             begin match lev with
             | None ->
 	      ([Feedback.msg_info ?loc:None ,strbrk "Setting notation at level 0."],0)
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 86d6888061..93e4e89a12 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -113,8 +113,8 @@ open Pputils
   let pr_strict b = if b then str "strict " else mt ()
 
   let pr_set_entry_type pr = function
-    | ETName -> str"ident"
-    | ETReference -> str"global"
+    | ETIdent -> str"ident"
+    | ETGlobal -> str"global"
     | ETPattern (b,None) -> pr_strict b ++ str"pattern"
     | ETPattern (b,Some n) -> pr_strict b ++ str"pattern" ++ spc () ++ pr_at_level (NumLevel n)
     | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko