Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).

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

4 files changed, 77 insertions, 78 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ef18ad4ebb..087ae31ae6 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -31,7 +31,7 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
 
-let loc_of_binder_let = function
+let loc_of_binder = function
   | LocalRawAssum ((loc,_)::_,_,_)::_ -> loc
   | LocalRawDef ((loc,_),_)::_ -> loc
   | _ -> dummy_loc
@@ -87,8 +87,8 @@ let lpar_id_coloneq =
               | _ -> err ())
         | _ -> err ())
 
-let impl_ident =
-  Gram.Entry.of_parser "impl_ident"
+let impl_ident_head =
+  Gram.Entry.of_parser "impl_ident_head"
     (fun strm ->
       match get_tok (stream_nth 0 strm) with
 	| KEYWORD "{" ->
@@ -129,8 +129,8 @@ let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern lconstr_pattern Constr.ident
-  binder binder_let binders_let record_declaration
-  binders_let_fixannot typeclass_constraint pattern appl_arg;
+  closed_binder binders binders_fixannot
+  record_declaration typeclass_constraint pattern appl_arg;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -232,13 +232,13 @@ GEXTEND Gram
       (id, Topconstr.abstract_constr_expr c (binders_of_lidents params)) ] ]
   ;
   binder_constr:
-    [ [ forall; bl = binder_list; ","; c = operconstr LEVEL "200" ->
+    [ [ forall; bl = open_binders; ","; c = operconstr LEVEL "200" ->
           mkCProdN loc bl c
-      | lambda; bl = binder_list; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
+      | lambda; bl = open_binders; [ "=>" | "," ]; c = operconstr LEVEL "200" ->
           mkCLambdaN loc bl c
-      | "let"; id=name; bl = binders_let; ty = type_cstr; ":=";
+      | "let"; id=name; bl = binders; ty = type_cstr; ":=";
         c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
-          let loc1 = loc_of_binder_let bl in
+          let loc1 = loc_of_binder bl in
           CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
       | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" ->
           let fixp = mk_single_fix fx in
@@ -296,7 +296,7 @@ GEXTEND Gram
       | "cofix" -> false ] ]
   ;
   fix_decl:
-    [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":=";
+    [ [ id=identref; bl=binders_fixannot; ty=type_cstr; ":=";
         c=operconstr LEVEL "200" ->
           (id,fst bl,snd bl,c,ty) ] ]
   ;
@@ -363,15 +363,7 @@ GEXTEND Gram
       | n = INT -> CPatPrim (loc, Numeral (Bigint.of_string n))
       | s = string -> CPatPrim (loc, String s) ] ]
   ;
-  binder_list:
-    [ [ idl=LIST1 name; bl=binders_let ->
-      LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl
-    | idl=LIST1 name; ":"; c=lconstr ->
-        [LocalRawAssum (idl,Default Explicit,c)]
-    | cl = binders_let -> cl
-    ] ]
-  ;
-  binder_assum:
+  impl_ident_tail:
     [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None))
     | idl=LIST1 name; ":"; c=lconstr; "}" ->
         (fun id -> LocalRawAssum (id::idl,Default Implicit,c))
@@ -388,47 +380,56 @@ GEXTEND Gram
 	rel=OPT constr; "}" -> (id, CMeasureRec (m,rel))
     ] ]
   ;
-  binders_let_fixannot:
-    [ [ id=impl_ident; assum=binder_assum; bl = binders_let_fixannot ->
-	(assum (loc, Name id) :: fst bl), snd bl
-    | f = fixannot -> [], f
-    | b = binder_let; bl = binders_let_fixannot -> b @ fst bl, snd bl
-    | -> [], (None, CStructRec)
+  binders_fixannot:
+    [ [ id = impl_ident_head; assum = impl_ident_tail; bl = binders_fixannot ->
+          (assum (loc, Name id) :: fst bl), snd bl
+      | f = fixannot -> [], f
+      | b = binder; bl = binders_fixannot -> b @ fst bl, snd bl
+      | -> [], (None, CStructRec)
     ] ]
   ;
-  binders_let:
-    [ [ b = binder_let; bl = binders_let -> b @ bl
-    | -> [] ] ]
-  ;
-  binder_let:
-    [ [ id=name ->
-      [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
-    | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
-        [LocalRawAssum (id::idl,Default Explicit,c)]
-    | "("; id=name; ":"; c=lconstr; ")" ->
-        [LocalRawAssum ([id],Default Explicit,c)]
-    | "("; id=name; ":="; c=lconstr; ")" ->
-        [LocalRawDef (id,c)]
-    | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-        [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
-    | "{"; id=name; "}" ->
-        [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
-    | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
-        [LocalRawAssum (id::idl,Default Implicit,c)]
-    | "{"; id=name; ":"; c=lconstr; "}" ->
-        [LocalRawAssum ([id],Default Implicit,c)]
-    | "{"; id=name; idl=LIST1 name; "}" ->
-        List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
-    | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
-    | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
-	List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
+  open_binders:
+    (* Same as binders but parentheses around a closed binder are optional if
+       the latter is unique *)
+    [ [ (* open binder *)
+        idl = LIST1 name; ":"; c = lconstr ->
+          [LocalRawAssum (idl,Default Explicit,c)]
+	(* binders factorized with open binder *)
+      | idl = LIST1 name; bl = binders ->
+          let t = CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))) in
+          LocalRawAssum (idl,Default Explicit,t)::bl
+      | bl = closed_binder; bl' = binders ->
+	  bl@bl'
     ] ]
   ;
+  binders:
+    [ [ l = LIST0 binder -> List.flatten l ] ]
+  ;
   binder:
-    [ [ id=name -> ([id],Default Explicit,CHole (loc, None))
-      | "("; idl=LIST1 name; ":"; c=lconstr; ")" -> (idl,Default Explicit,c)
-      | "{"; idl=LIST1 name; ":"; c=lconstr; "}" -> (idl,Default Implicit,c)
+    [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (loc, None))]
+      | bl = closed_binder -> bl ] ]
+  ;
+  closed_binder:
+    [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" ->
+          [LocalRawAssum (id::idl,Default Explicit,c)]
+      | "("; id=name; ":"; c=lconstr; ")" ->
+          [LocalRawAssum ([id],Default Explicit,c)]
+      | "("; id=name; ":="; c=lconstr; ")" ->
+          [LocalRawDef (id,c)]
+      | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
+          [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
+      | "{"; id=name; "}" ->
+          [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
+      | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
+          [LocalRawAssum (id::idl,Default Implicit,c)]
+      | "{"; id=name; ":"; c=lconstr; "}" ->
+          [LocalRawAssum ([id],Default Implicit,c)]
+      | "{"; id=name; idl=LIST1 name; "}" ->
+          List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl)
+      | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
+	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc
+      | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
+	  List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc
     ] ]
   ;
   typeclass_constraint:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 359d2321d3..3e5a52e468 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -141,9 +141,9 @@ GEXTEND Gram
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = identref; bl = binders_let; ":"; c = lconstr;
+    [ [ thm = thm_token; id = identref; bl = binders; ":"; c = lconstr;
         l = LIST0
-          [ "with"; id = identref; bl = binders_let; ":"; c = lconstr ->
+          [ "with"; id = identref; bl = binders; ":"; c = lconstr ->
             (Some id,(bl,c,None)) ] ->
           VernacStartTheoremProof (thm,(Some id,(bl,c,None))::l, false, no_hook)
       | stre = assumption_token; nl = inline; bl = assum_list ->
@@ -177,7 +177,7 @@ GEXTEND Gram
   ;
   gallina_ext:
     [ [ b = record_token; infer = infer_token; oc = opt_coercion; name = identref;
-        ps = binders_let;
+        ps = binders;
 	s = OPT [ ":"; s = lconstr -> s ];
 	cfs = [ ":="; l = constructor_list_or_record_decl -> l
 	  | -> RecordDecl (None, []) ] ->
@@ -238,13 +238,13 @@ GEXTEND Gram
   ;
   (* Simple definitions *)
   def_body:
-    [ [ bl = binders_let; ":="; red = reduce; c = lconstr ->
+    [ [ bl = binders; ":="; red = reduce; c = lconstr ->
       (match c with
           CCast(_,c, Rawterm.CastConv (k,t)) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
-    | bl = binders_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
+    | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
 	DefineBody (bl, red, c, Some t)
-    | bl = binders_let; ":"; t = lconstr ->
+    | bl = binders; ":"; t = lconstr ->
         ProveBody (bl, t) ] ]
   ;
   reduce:
@@ -261,7 +261,7 @@ GEXTEND Gram
   ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = identref; oc = opt_coercion; indpar = binders_let;
+    [ [ id = identref; oc = opt_coercion; indpar = binders;
         c = OPT [ ":"; c = lconstr -> c ];
         ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
 	   (((oc,id),indpar,c,lc),ntn) ] ]
@@ -288,13 +288,13 @@ GEXTEND Gram
   (* (co)-fixpoints *)
   rec_definition:
     [ [ id = identref;
-	bl = binders_let_fixannot;
+	bl = binders_fixannot;
         ty = type_cstr;
 	def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
 	  let bl, annot = bl in ((id,annot,bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = identref; bl = binders_let; ty = type_cstr; 
+    [ [ id = identref; bl = binders; ty = type_cstr;
         def = OPT [":="; def = lconstr -> def]; ntn = decl_notation ->
           ((id,bl,ty,def),ntn) ] ]
   ;
@@ -335,12 +335,12 @@ GEXTEND Gram
     [ [ bd = record_binder; ntn = decl_notation -> bd,ntn ] ]
   ;
   record_binder_body:
-    [ [ l = binders_let; oc = of_type_with_opt_coercion;
+    [ [ l = binders; oc = of_type_with_opt_coercion;
          t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN loc l t))
-      | l = binders_let; oc = of_type_with_opt_coercion;
+      | l = binders; oc = of_type_with_opt_coercion;
          t = lconstr; ":="; b = lconstr -> fun id ->
 	   (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
-      | l = binders_let; ":="; b = lconstr -> fun id ->
+      | l = binders; ":="; b = lconstr -> fun id ->
          match b with
 	 | CCast(_,b, Rawterm.CastConv (_, t)) ->
 	     (false,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
@@ -363,7 +363,7 @@ GEXTEND Gram
   ;
 
   constructor_type:
-    [[ l = binders_let;
+    [[ l = binders;
       t= [ coe = of_type_with_opt_coercion; c = lconstr ->
 	            fun l id -> (coe,(id,mkCProdN loc l c))
             |  ->
@@ -538,7 +538,7 @@ GEXTEND Gram
          t = class_rawexpr ->
 	  VernacCoercion (use_locality_exp (), ByNotation ntn, s, t)
 
-      | IDENT "Context"; c = binders_let ->
+      | IDENT "Context"; c = binders ->
 	  VernacContext c
 
       | IDENT "Instance"; namesup = instance_name; ":";
@@ -588,7 +588,7 @@ GEXTEND Gram
       | IDENT "transparent" -> Conv_oracle.transparent ] ]
   ;
   instance_name:
-    [ [ name = identref; sup = OPT binders_let ->
+    [ [ name = identref; sup = OPT binders ->
 	  (let (loc,id) = name in (loc, Name id)),
           (Option.default [] sup)
       | -> (loc, Anonymous), []  ] ]
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b0e4fc1f15..3cdf89ebd3 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -354,10 +354,9 @@ module Constr =
     let pattern = Gram.entry_create "constr:pattern"
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
-    let binder = Gram.entry_create "constr:binder"
-    let binder_let = Gram.entry_create "constr:binder_let"
-    let binders_let = Gram.entry_create "constr:binders_let"
-    let binders_let_fixannot = Gram.entry_create "constr:binders_let_fixannot"
+    let closed_binder = Gram.entry_create "constr:closed_binder"
+    let binders = Gram.entry_create "constr:binders"
+    let binders_fixannot = Gram.entry_create "constr:binders_fixannot"
     let typeclass_constraint = Gram.entry_create "constr:typeclass_constraint"
     let record_declaration = Gram.entry_create "constr:record_declaration"
     let appl_arg = Gram.entry_create "constr:appl_arg"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 1436b0e189..99c155e8d5 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -196,10 +196,9 @@ module Constr :
     val pattern : cases_pattern_expr Gram.entry
     val constr_pattern : constr_expr Gram.entry
     val lconstr_pattern : constr_expr Gram.entry
-    val binder : (name located list * binder_kind * constr_expr) Gram.entry
-    val binder_let : local_binder list Gram.entry
-    val binders_let : local_binder list Gram.entry
-    val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry
+    val closed_binder : local_binder list Gram.entry
+    val binders : local_binder list Gram.entry
+    val binders_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.entry
     val typeclass_constraint : (name located * bool * constr_expr) Gram.entry
     val record_declaration : constr_expr Gram.entry
     val appl_arg : (constr_expr * explicitation located option) Gram.entry