- Structuring Numbers and fixing Setoid in stdlib's doc.

- Adding ability to use "_" in syntax for binders (as in "exists _:nat, True").



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

16 files changed, 159 insertions, 115 deletions

diff --git a/CHANGES b/CHANGES
index 593bae43c..2e747ce8b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -92,7 +92,7 @@ Vernacular commands
 - Specific sort constraints on Record now taken into account.
 - "Print LoadPath" supports a path argument to filter the display.
 
-Libraries (DOC TO CHECK)
+Libraries
 
 - Several parts of the libraries are now in Type, in particular FSets,
   SetoidList, ListSet, Sorting, Zmisc. This may induce a few
@@ -195,6 +195,7 @@ Libraries (DOC TO CHECK)
   contribution repository (contribution CoC_History). New lemmas about 
   transitive closure added and some bound variables renamed (exceptional
   risk of incompatibilities).
+- Syntax for binders in terms (e.g. for "exists") supports anonymous names.
 
 Notations, coercions, implicit arguments and type inference
 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 68460c76e..71cef59e2 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1588,7 +1588,7 @@ let xlate_syntax_modifier = function
   | Extend.SetEntryType(x,typ) ->
       CT_entry_type(CT_ident x,
 		 match typ with
-		     Extend.ETIdent -> CT_ident "ident"
+		     Extend.ETName -> CT_ident "ident"
 		   | Extend.ETReference -> CT_ident "global"
 		   | Extend.ETBigint -> CT_ident "bigint"
 		   | _ -> xlate_error "syntax_type not parsed")
diff --git a/dev/base_include b/dev/base_include
index 0b7a0b67d..d4366843f 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -128,7 +128,6 @@ open Hipattern
 open Inv
 open Leminv
 open Refine
-open Setoid_replace
 open Tacinterp
 open Tacticals
 open Tactics
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index cae948a00..d35fb199b 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -8,7 +8,8 @@ A few differences in Coq ML interfaces between Coq V8.1 and V8.2
 ** Datatypes
 
 List of occurrences moved from "int list" to "Termops.occurrences" (an
-alias to "bool * int list").
+  alias to "bool * int list")
+ETIdent renamed to ETName
 
 ** Functions
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 6ade546b0..77eb29285 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -36,7 +36,7 @@ string \verb="A /\ B"= (called a {\em notation}) tells how it is
 symbolically written.
 
 A notation is always surrounded by double quotes (excepted when the
-abbreviation is a single ident, see \ref{Abbreviations}). The
+abbreviation is a single identifier, see \ref{Abbreviations}). The
 notation is composed of {\em tokens} separated by spaces.  Identifiers
 in the string (such as \texttt{A} and \texttt{B}) are the {\em
 parameters} of the notation. They must occur at least once each in the
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 64bf252f2..6b35dfa99 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -180,86 +180,103 @@ through the <tt>Require Import</tt> command.</p>
   </dd>
 
   <dt> <b>Numbers</b>: 
-    A modular axiomatic construction for numbers
+    An experimental modular architecture for arithmetic
   </dt>
-  <dd>
-  theories/Numbers/NumPrelude.v
-  theories/Numbers/BigNumPrelude.v
-  theories/Numbers/NaryFunctions.v
-  </dd>
-  
-  <dd>
-theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
-theories/Numbers/Cyclic/Abstract/NZCyclic.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
-theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
-theories/Numbers/Cyclic/Int31/Cyclic31.v
-theories/Numbers/Cyclic/Int31/Int31.v
-theories/Numbers/Cyclic/ZModulo/ZModulo.v
-  </dd>
+    <dt> <b>&nbsp;&nbsp;Prelude</b>: 
+    <dd>
+    theories/Numbers/NumPrelude.v
+    theories/Numbers/BigNumPrelude.v
+    theories/Numbers/NaryFunctions.v
+    </dd>
 
-  <dd>
-    theories/Numbers/Integer/Abstract/ZAdd.v
-theories/Numbers/Integer/Abstract/ZAddOrder.v
-theories/Numbers/Integer/Abstract/ZAxioms.v
-theories/Numbers/Integer/Abstract/ZBase.v
-theories/Numbers/Integer/Abstract/ZDomain.v
-theories/Numbers/Integer/Abstract/ZLt.v
-theories/Numbers/Integer/Abstract/ZMul.v
-theories/Numbers/Integer/Abstract/ZMulOrder.v
-theories/Numbers/Integer/BigZ/BigZ.v
-theories/Numbers/Integer/BigZ/ZMake.v
-theories/Numbers/Integer/Binary/ZBinary.v
-theories/Numbers/Integer/NatPairs/ZNatPairs.v
-theories/Numbers/Integer/SpecViaZ/ZSig.v
-theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
-  </dd>
+    <dt> <b>&nbsp;&nbsp;NatInt</b>:
+       Abstract mixed natural/integer/cyclic arithmetic
+    <dd>
+    theories/Numbers/NatInt/NZAdd.v
+    theories/Numbers/NatInt/NZAddOrder.v
+    theories/Numbers/NatInt/NZAxioms.v
+    theories/Numbers/NatInt/NZBase.v
+    theories/Numbers/NatInt/NZMul.v
+    theories/Numbers/NatInt/NZMulOrder.v
+    theories/Numbers/NatInt/NZOrder.v
+    </dd>
+    </dt>
 
-  <dd>
-theories/Numbers/NatInt/NZAdd.v
-theories/Numbers/NatInt/NZAddOrder.v
-theories/Numbers/NatInt/NZAxioms.v
-theories/Numbers/NatInt/NZBase.v
-theories/Numbers/NatInt/NZMul.v
-theories/Numbers/NatInt/NZMulOrder.v
-theories/Numbers/NatInt/NZOrder.v
-  </dd>
+    <dt> <b>&nbsp;&nbsp;Cyclic</b>: 
+       Abstract and 31-bits-based cyclic arithmetic
+    <dd>
+    theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+    theories/Numbers/Cyclic/Abstract/NZCyclic.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleAdd.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleLift.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleMul.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleSqrt.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleSub.v
+    theories/Numbers/Cyclic/DoubleCyclic/DoubleType.v
+    theories/Numbers/Cyclic/Int31/Cyclic31.v
+    theories/Numbers/Cyclic/Int31/Int31.v
+    theories/Numbers/Cyclic/ZModulo/ZModulo.v
+    </dd>
+    </dt>
 
-  <dd>
-theories/Numbers/Natural/Abstract/NAdd.v
-theories/Numbers/Natural/Abstract/NAddOrder.v
-theories/Numbers/Natural/Abstract/NAxioms.v
-theories/Numbers/Natural/Abstract/NBase.v
-theories/Numbers/Natural/Abstract/NDefOps.v
-theories/Numbers/Natural/Abstract/NIso.v
-theories/Numbers/Natural/Abstract/NMul.v
-theories/Numbers/Natural/Abstract/NMulOrder.v
-theories/Numbers/Natural/Abstract/NOrder.v
-theories/Numbers/Natural/Abstract/NStrongRec.v
-theories/Numbers/Natural/Abstract/NSub.v
-theories/Numbers/Natural/BigN/BigN.v
-theories/Numbers/Natural/BigN/Nbasic.v
-theories/Numbers/Natural/BigN/NMake.v
-theories/Numbers/Natural/Binary/NBinary.v
-theories/Numbers/Natural/Binary/NBinDefs.v
-theories/Numbers/Natural/Peano/NPeano.v
-theories/Numbers/Natural/SpecViaZ/NSig.v
-theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
-  </dd>
+    <dt> <b>&nbsp;&nbsp;Natural</b>: 
+       Abstract and 31-bits-words-based natural arithmetic
+    <dd>
+    theories/Numbers/Natural/Abstract/NAdd.v
+    theories/Numbers/Natural/Abstract/NAddOrder.v
+    theories/Numbers/Natural/Abstract/NAxioms.v
+    theories/Numbers/Natural/Abstract/NBase.v
+    theories/Numbers/Natural/Abstract/NDefOps.v
+    theories/Numbers/Natural/Abstract/NIso.v
+    theories/Numbers/Natural/Abstract/NMul.v
+    theories/Numbers/Natural/Abstract/NMulOrder.v
+    theories/Numbers/Natural/Abstract/NOrder.v
+    theories/Numbers/Natural/Abstract/NStrongRec.v
+    theories/Numbers/Natural/Abstract/NSub.v
+    theories/Numbers/Natural/Binary/NBinary.v
+    theories/Numbers/Natural/Binary/NBinDefs.v
+    theories/Numbers/Natural/Peano/NPeano.v
+    theories/Numbers/Natural/SpecViaZ/NSig.v
+    theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+    theories/Numbers/Natural/BigN/BigN.v
+    theories/Numbers/Natural/BigN/Nbasic.v
+    theories/Numbers/Natural/BigN/NMake.v
+    </dd>
+    </dt>
 
-  <dd>
+    <dt> <b>&nbsp;&nbsp;Integer</b>: 
+       Abstract and concrete (especially 31-bits-words-based) integer arithmetic
+    <dd>
+    theories/Numbers/Integer/Abstract/ZAdd.v
+    theories/Numbers/Integer/Abstract/ZAddOrder.v
+    theories/Numbers/Integer/Abstract/ZAxioms.v
+    theories/Numbers/Integer/Abstract/ZBase.v
+    theories/Numbers/Integer/Abstract/ZDomain.v
+    theories/Numbers/Integer/Abstract/ZLt.v
+    theories/Numbers/Integer/Abstract/ZMul.v
+    theories/Numbers/Integer/Abstract/ZMulOrder.v
+    theories/Numbers/Integer/Binary/ZBinary.v
+    theories/Numbers/Integer/NatPairs/ZNatPairs.v
+    theories/Numbers/Integer/SpecViaZ/ZSig.v
+    theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+    theories/Numbers/Integer/BigZ/BigZ.v
+    theories/Numbers/Integer/BigZ/ZMake.v
+    </dd>
+    </dt>
+
+    <dt><b>&nbsp;&nbsp;Rational</b>:
+       Abstract and 31-bits-words-based rational arithmetic
+    <dd>
+    theories/Numbers/Rational/SpecViaQ/QSig.v
     theories/Numbers/Rational/BigQ/BigQ.v
     theories/Numbers/Rational/BigQ/QMake.v
-    theories/Numbers/Rational/SpecViaQ/QSig.v
-  </dd>
+    </dd>
+    </dt>
+  </dt>
   
   <dt> <b>Relations</b>:
        Relations (definitions and basic results)
@@ -318,8 +335,6 @@ theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
   <dt> <b>Setoids</b>:
   <dd> 
     theories/Setoids/Setoid.v
-    theories/Setoids/Setoid_Prop.v
-    theories/Setoids/Setoid_tac.v
   </dd>
     
   <dt> <b>Lists</b>:
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c658faa0f..87768c419 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -191,11 +191,14 @@ let set_var_scope loc id (_,_,scopt,scopes) varscopes =
 (**********************************************************************)
 (* Syntax extensions                                                  *)
 
-let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) id =
+let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env))=
+ function
+ | Anonymous -> (renaming,env),Anonymous
+ | Name id ->
   try
     (* Binders bound in the notation are considered first-order objects *)
-    let _,id' = coerce_to_id (fst (List.assoc id subst)) in
-    (renaming,(Idset.add id' ids,unb,tmpsc,scopes)), id'
+    let _,na = coerce_to_name (fst (List.assoc id subst)) in
+    (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -205,7 +208,7 @@ let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env)) i
     let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
     let id' = next_ident_away id fvs in
     let renaming' = if id=id' then renaming else (id,id')::renaming in
-    (renaming',env), id'
+    (renaming',env), Name id'
 
 let rec subst_iterator y t = function
   | RVar (_,id) as x -> if id = y then t else x
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 6bee22f6c..d31230552 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -53,11 +53,17 @@ type aconstr =
 (**********************************************************************)
 (* Re-interpret a notation as a rawconstr, taking care of binders     *)
 
+let name_to_ident = function
+  | Anonymous -> error "This expression should be a simple identifier."
+  | Name id -> id 
+
+let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
+
 let rec cases_pattern_fold_map loc g e = function
   | PatVar (_,na) ->
-      let e',na' = name_fold_map g e na in e', PatVar (loc,na')
+      let e',na' = g e na in e', PatVar (loc,na')
   | PatCstr (_,cstr,patl,na) ->
-      let e',na' = name_fold_map g e na in
+      let e',na' = g e na in
       let e',patl' = list_fold_map (cases_pattern_fold_map loc g) e patl in
       e', PatCstr (loc,cstr,patl',na')
 
@@ -77,38 +83,38 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let outerl = (ldots_var,inner)::(if swap then [x,RVar(loc,y)] else []) in
       subst_rawvars outerl it
   | ALambda (na,ty,c) ->
-      let e,na = name_fold_map g e na in RLambda (loc,na,Explicit,f e ty,f e c)
+      let e,na = g e na in RLambda (loc,na,Explicit,f e ty,f e c)
   | AProd (na,ty,c) ->
-      let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
+      let e,na = g e na in RProd (loc,na,Explicit,f e ty,f e c)
   | ALetIn (na,b,c) ->
-      let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
+      let e,na = g e na in RLetIn (loc,na,f e b,f e c)
   | ACases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
 	| Some (ind,npar,nal) -> 
 	  let e',nal' = List.fold_right (fun na (e',nal) -> 
-	      let e',na' = name_fold_map g e' na in e',na'::nal) nal (e',[]) in
+	      let e',na' = g e' na in e',na'::nal) nal (e',[]) in
 	  e',Some (loc,ind,npar,nal') in
-	let e',na' = name_fold_map g e' na in
+	let e',na' = g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
-      let fold (idl,e) id = let (e,id) = g e id in ((id::idl,e),id) in
+      let fold (nal,e) na = let (e,na) = g e na in ((name_to_ident na::nal,e),na) in
       let eqnl' = List.map (fun (patl,rhs) ->
 	let ((idl,e),patl) =
 	  list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
 	(loc,idl,patl,f e rhs)) eqnl in
       RCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
   | ALetTuple (nal,(na,po),b,c) ->
-      let e,nal = list_fold_map (name_fold_map g) e nal in 
-      let e,na = name_fold_map g e na in
+      let e,nal = list_fold_map g e nal in 
+      let e,na = g e na in
       RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
   | AIf (c,(na,po),b1,b2) ->
-      let e,na = name_fold_map g e na in
+      let e,na = g e na in
       RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
   | ARec (fk,idl,dll,tl,bl) ->
-      let e,idl = array_fold_map g e idl in
+      let e,idl = array_fold_map (to_id g) e idl in
       let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
-	  let e,na = name_fold_map g e na in
+	  let e,na = g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
       RRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e) bl)
   | ACast (c,k) -> RCast (loc,f e c, 
@@ -452,9 +458,13 @@ let match_opt f sigma t1 t2 = match (t1,t2) with
   | Some t1, Some t2 -> f sigma t1 t2
   | _ -> raise No_match
 
+let rawconstr_of_name = function
+  | Anonymous -> RHole (dummy_loc,Evd.InternalHole)
+  | Name id -> RVar (dummy_loc,id)
+
 let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
-  | (Name id1,Name id2) when List.mem id2 metas ->
-      alp, bind_env alp sigma id2 (RVar (dummy_loc,id1))
+  | (na,Name id2) when List.mem id2 metas ->
+      alp, bind_env alp sigma id2 (rawconstr_of_name na)
   | (Name id1,Name id2) -> (id1,id2)::alp,sigma
   | (Anonymous,Anonymous) -> alp,sigma
   | _ -> raise No_match
@@ -886,6 +896,13 @@ let coerce_to_id = function
         (constr_loc a,"coerce_to_id",
          str "This expression should be a simple identifier.")
 
+let coerce_to_name = function
+  | CRef (Ident (loc,id)) -> (loc,Name id)
+  | CHole (loc,_) -> (loc,Anonymous)
+  | a -> user_err_loc
+        (constr_loc a,"coerce_to_name",
+         str "This expression should be a name.")
+
 (* Used in correctness and interface *)
 
 let map_binder g e nal = List.fold_right (fun (_,na) -> name_fold g na) nal e
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index cecea239c..303926967 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -62,7 +62,7 @@ val eq_rawconstr : rawconstr -> rawconstr -> bool
 (* Re-interpret a notation as a rawconstr, taking care of binders     *)
 
 val rawconstr_of_aconstr_with_binders : loc -> 
-  ('a -> identifier -> 'a * identifier) ->
+  ('a -> name -> 'a * name) ->
   ('a -> aconstr -> rawconstr) -> 'a -> aconstr -> rawconstr
 
 val rawconstr_of_aconstr : loc -> aconstr -> rawconstr
@@ -201,6 +201,7 @@ val mkLetInC : name located * constr_expr * constr_expr -> constr_expr
 val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr
 
 val coerce_to_id : constr_expr -> identifier located
+val coerce_to_name : constr_expr -> name located
 
 val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 585d7ab82..b784acdc3 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -47,6 +47,14 @@ open Vernacexpr
 (**********************************************************************)
 (** Declare Notations grammar rules                                   *)
 
+let constr_expr_of_name (loc,na) = match na with
+  | Anonymous -> CHole (loc,None)
+  | Name id -> CRef (Ident (loc,id))
+
+let cases_pattern_expr_of_name (loc,na) = match na with
+  | Anonymous -> CPatAtom (loc,None)
+  | Name id -> CPatAtom (loc,Some (Ident (loc,id)))
+
 type prod_item =
   | Term of Token.pattern
   | NonTerm of constr_production_entry * 
@@ -65,9 +73,9 @@ let make_constr_action
         Gramext.action (fun (v:constr_expr) -> make (v :: env, envlist) tl)
     | Some (p, ETReference) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:reference) -> make (CRef v :: env, envlist) tl)
-    | Some (p, ETIdent) :: tl -> (* non-terminal *)
-        Gramext.action (fun (v:identifier) ->
-	  make (CRef (Ident (dummy_loc,v)) :: env, envlist) tl)
+    | Some (p, ETName) :: tl -> (* non-terminal *)
+        Gramext.action (fun (na:name located) ->
+	  make (constr_expr_of_name na :: env, envlist) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bigint.bigint) ->
 	  make (CPrim (dummy_loc,Numeral v) :: env, envlist) tl)
@@ -89,10 +97,9 @@ let make_cases_pattern_action
     | Some (p, ETReference) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:reference) ->
 	  make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
-    | Some (p, ETIdent) :: tl -> (* non-terminal *)
-        Gramext.action (fun (v:identifier) ->
-	  make 
-	    (CPatAtom (dummy_loc,Some (Ident (dummy_loc,v)))::env, envlist) tl)
+    | Some (p, ETName) :: tl -> (* non-terminal *)
+        Gramext.action (fun (na:name located) ->
+	  make (cases_pattern_expr_of_name na :: env, envlist) tl)
     | Some (p, ETBigint) :: tl -> (* non-terminal *)
         Gramext.action (fun (v:Bigint.bigint) ->
 	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
diff --git a/parsing/extend.ml b/parsing/extend.ml
index b62e23b5e..36e1000b1 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -31,7 +31,7 @@ type production_level =
   | NumLevel of int
 
 type ('lev,'pos) constr_entry_key =
-  | ETIdent | ETReference | ETBigint
+  | ETName | ETReference | ETBigint
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 1fc8800ef..61fee077a 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -24,7 +24,7 @@ type production_level =
   | NumLevel of int
 
 type ('lev,'pos) constr_entry_key =
-  | ETIdent | ETReference | ETBigint
+  | ETName | ETReference | ETBigint
   | ETConstr of ('lev * 'pos)
   | ETPattern
   | ETOther of string * string
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 2b99fee97..ff6d998e2 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -852,7 +852,7 @@ GEXTEND Gram
       | IDENT "format"; s = [s = STRING -> (loc,s)] -> SetFormat s ] ]
   ;
   syntax_extension_type:
-    [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
+    [ [ IDENT "ident" -> ETName | IDENT "global" -> ETReference
       | IDENT "bigint" -> ETBigint
     ] ]
   ;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d81727487..cab5c1a5d 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -690,7 +690,7 @@ let compute_entry allow_create adjust forpat = function
       (if forpat then weaken_entry Constr.pattern
        else weaken_entry Constr.operconstr),
       adjust (n,q), false
-  | ETIdent -> weaken_entry Constr.ident, None, false
+  | ETName -> weaken_entry Prim.name, None, false
   | ETBigint -> weaken_entry Prim.bigint, None, false
   | ETReference -> weaken_entry Constr.global, None, false
   | ETPattern -> weaken_entry Constr.pattern, None, false
@@ -722,7 +722,7 @@ let is_self from e =
       ETConstr(n,()), ETConstr(NumLevel n',
         BorderProd(Right, _ (* Some(Gramext.NonA|Gramext.LeftA) *))) -> false
     | ETConstr(n,()), ETConstr(NumLevel n',BorderProd(Left,_)) -> n=n'
-    | (ETIdent,ETIdent | ETReference, ETReference | ETBigint,ETBigint
+    | (ETName,ETName | ETReference, ETReference | ETBigint,ETBigint
       | ETPattern, ETPattern) -> true
     | ETOther(s1,s2), ETOther(s1',s2') -> s1=s1' & s2=s2'
     | _ -> false
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0a4cd5e29..496af5b6e 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -105,7 +105,7 @@ let pr_prec = function
   | None -> mt()
 
 let pr_set_entry_type = function
-  | ETIdent -> str"ident"
+  | ETName -> str"ident"
   | ETReference -> str"global"
   | ETPattern -> str"pattern"
   | ETConstr _ -> str"constr"
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 234dd04c4..75a6a8e75 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -743,7 +743,7 @@ let set_entry_type etyps (x,typ) =
       | ETConstr (n,()), (_,BorderProd (left,_)) ->
           ETConstr (n,BorderProd (left,None))
       | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
-      | (ETPattern | ETIdent | ETBigint | ETOther _ | ETReference as t), _ -> t
+      | (ETPattern | ETName | ETBigint | ETOther _ | ETReference as t), _ -> t
       | (ETConstrList _, _) -> assert false
     with Not_found -> ETConstr typ
   in (x,typ)
@@ -764,7 +764,7 @@ let find_precedence lev etyps symbols =
       (try match List.assoc x etyps with
 	| ETConstr _ ->
 	    error "The level of the leftmost non-terminal cannot be changed."
-	| ETIdent | ETBigint | ETReference -> 
+	| ETName | ETBigint | ETReference -> 
 	    if lev = None then 
 	      Flags.if_verbose msgnl (str "Setting notation at level 0.")
 	    else