- 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

6 files changed, 20 insertions, 13 deletions

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"