Nouvelle mouture du traducteur v7->v8

Option -v8 à coqtop lance coqtopnew
Le terminateur reste "." en v8
Ajout construction primitive CLetTuple/RLetTuple
Introduction typage dans le traducteur pour traduire les Case/Cases/Match
Ajout mutables dans RCases or ROrderedCase pour permettre la traduction
Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts
+ Bugs ou améliorations diverses
Raffinement affichage projections de Record/Structure.


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

17 files changed, 206 insertions, 137 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 3971892714..60848fdfd0 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -284,12 +284,17 @@ let subst_constr_expr a loc subs =
   | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _ 
   | CNumeral _ | CDynamic _ | CRef _ as x -> x
-  | CCases (_,po,a,bl) ->
+  | CCases (_,(po,rtntypo),a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
       let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in
-      CCases (loc,option_app subst po,List.map subst a,bl)
+      CCases (loc,(option_app subst po,option_app subst rtntypo),
+        List.map (fun (tm,x) -> subst tm,x) a,bl)
   | COrderedCase (_,s,po,a,bl) ->
       COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl)
+  | CLetTuple (_,nal,(na,po),a,b) ->
+      let na = name_app (subst_id subs) na in
+      let nal = List.map (name_app (subst_id subs)) nal in
+      CLetTuple (loc,nal,(na,option_app subst po),subst a,subst b)
   | CFix (_,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,subst t,subst d)) dl)
   | CCoFix (_,id,dl) ->
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 679d174c2a..4d4000b238 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -55,13 +55,17 @@ GEXTEND Gram
   operconstr: LEVEL "1"
     [ [ "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of";
         OPT "|"; eqs = ne_eqn_list; "end" ->
-	  CCases (loc, Some p, lc, eqs)
+          let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in
+	  CCases (loc, (Some p,None), lc, eqs)
       | "Cases"; lc = LIST1 constr; "of";
 	OPT "|"; eqs = ne_eqn_list; "end" ->
-	  CCases (loc, None, lc, eqs)
+          let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in
+	  CCases (loc, (None,None), lc, eqs)
       | "<"; p = annot; ">"; "Cases"; lc = LIST1 constr; "of"; "end" ->
-	  CCases (loc, Some p, lc, [])
+          let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in
+	  CCases (loc, (Some p,None), lc, [])
       | "Cases"; lc = LIST1 constr; "of"; "end" -> 
-	  CCases (loc, None, lc, []) ] ]
+          let lc = List.map (fun c -> c,(Names.Anonymous,None)) lc in
+	  CCases (loc, (None,None), lc, []) ] ]
   ;
 END;
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 43dc060a5a..5904906b01 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -127,12 +127,12 @@ GEXTEND Gram
   operconstr:
     [ "10" RIGHTA
       [ "!"; f = global; args = LIST0 (operconstr LEVEL "9") ->
-          CAppExpl (loc, (false,f), args)
+          CAppExpl (loc, (None,f), args)
 (*
       | "!"; f = global; "with"; b = binding_list ->
 	  <:ast< (APPLISTWITH $f $b) >>
 *)
-      | f = operconstr; args = LIST1 constr91 -> CApp (loc, (false,f), args) ]
+      | f = operconstr; args = LIST1 constr91 -> CApp (loc, (None,f), args) ]
     | "9" RIGHTA
       [ c1 = operconstr; "::"; c2 = operconstr LEVEL "9" -> CCast (loc, c1, c2) ]
     | "8" RIGHTA
@@ -196,7 +196,7 @@ GEXTEND Gram
       | "("; lc1 = lconstr; ")"; "@"; "["; cl = ne_constr_list; "]" ->
 	  (match lc1 with
 	    | CPatVar (loc2,(false,n)) -> 
-                CApp (loc,(false,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl)
+                CApp (loc,(None,CPatVar (loc2, (true,n))), List.map (fun c -> c, None) cl)
 	    | _ ->
 	    Util.error "Second-order pattern-matching expects a head metavariable")
       | IDENT "Fix"; id = identref; "{"; fbinders = fixbinders; "}" ->
@@ -208,7 +208,7 @@ GEXTEND Gram
       | s = sort -> CSort (loc, s)
       | v = global -> CRef v
       | n = bigint -> CNumeral (loc,n)
-      | "!"; f = global -> CAppExpl (loc,(false,f),[])
+      | "!"; f = global -> CAppExpl (loc,(None,f),[])
       | "'"; test_ident_colon; key = IDENT; ":"; c = constr; "'" -> 
           CDelimiters (loc,key,c) ] ]
   ;
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 16691158fe..f8bb62a22f 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -20,8 +20,9 @@ open Topconstr
 open Util
 
 let constr_kw =
-  [ "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as";
-    "let"; "if"; "then"; "else"; "struct"; "Prop"; "Set"; "Type"; ".(" ]
+  [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
+    "end"; "as"; "let"; "if"; "then"; "else"; "return";
+    "Prop"; "Set"; "Type"; ".(" ]
 let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
 let _ = Options.v7 := false
 
@@ -56,6 +57,7 @@ let match_bind_of_pat loc (oid,ty) =
   l1@l2
 
 let mk_match (loc,cil,rty,br) =
+(*
   let (lc,pargs) = List.split cil in
   let pr =
     match rty with
@@ -64,7 +66,8 @@ let mk_match (loc,cil,rty,br) =
           let idargs = (* TODO: not forget the list lengths for PP! *)
             List.flatten (List.map (match_bind_of_pat loc) pargs) in
           Some (CLambdaN(loc,idargs,ty)) in
-  CCases(loc,pr,lc,br)
+*)
+  CCases(loc,(None,rty),cil,br)
 
 let mk_fixb (loc,id,bl,ann,body,(tloc,tyc)) =
   let n =
@@ -101,9 +104,28 @@ let mk_fix(loc,kw,id,dcls) =
 let binder_constr =
   create_constr_entry (get_univ "constr") "binder_constr"
 
+
+let rec mkCProdN loc bll c =
+  match bll with
+  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
+      CProdN (loc,[idl,t],mkCProdN (join_loc loc1 loc) bll c)
+  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
+      CLetIn (loc,id,b,mkCProdN (join_loc loc1 loc) bll c)
+  | [] -> c
+  | LocalRawAssum ([],_) :: bll -> mkCProdN loc bll c
+
+let rec mkCLambdaN loc bll c =
+  match bll with
+  | LocalRawAssum ((loc1,_)::_ as idl,t) :: bll -> 
+      CLambdaN (loc,[idl,t],mkCLambdaN (join_loc loc1 loc) bll c)
+  | LocalRawDef ((loc1,_) as id,b) :: bll -> 
+      CLetIn (loc,id,b,mkCLambdaN (join_loc loc1 loc) bll c)
+  | [] -> c
+  | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
+
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
-  constr_pattern Constr.ident;
+  constr_pattern Constr.ident binder_let tuple_constr;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
@@ -130,6 +152,12 @@ GEXTEND Gram
   constr:
     [ [ c = operconstr LEVEL "9" -> c ] ]
   ;
+  tuple_constr:
+    [ 
+      [ (*c1 = tuple_constr; ","; c2 = tuple_constr ->
+         CNotation (loc,"_ , _",[c1;c2])
+      | *) c = operconstr -> c ] ]
+  ;
   operconstr:
     [ "200" RIGHTA
       [ c = binder_constr -> c ]
@@ -142,33 +170,39 @@ GEXTEND Gram
     | "40L" LEFTA
       [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ]
     | "10L" LEFTA
-      [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(false,f),args)
-      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(false,f),args) ]
+      [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
+      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args)
+      |	c=operconstr; ".("; f=global; args1=LIST0 appl_arg; ")";
+          args2=LIST0 appl_arg -> 
+	    CApp(loc,(Some (List.length args1+1),CRef f),args1@(c,None)::args2)
+      | c=operconstr; ".("; "@"; f=global; args1=LIST0 NEXT; ")";
+          args2=LIST0 NEXT -> 
+	    CAppExpl(loc,(Some (List.length args1+1),f),args1@c::args2) ]
     | "9" [ ]
     | "1L" LEFTA
-      [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c)
-      |	c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
-	  CApp(loc,(true,CRef f),args@[c,None])
-      | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT ->
-	  CAppExpl(loc,(false,f),args@[c]) ]
+      [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ]
     | "0"
       [ c=atomic_constr -> c
       | c=match_constr -> c
-      | "("; c=operconstr; ")" -> c ] ]
+      | "("; c=tuple_constr; ")" -> c ] ]
   ;
   binder_constr:
-    [ [ "!"; bl = binder_list; "."; c = operconstr LEVEL "200" ->
-          CProdN(loc,bl,c)
-      | "fun"; bl = LIST1 binder; ty = type_cstr; "=>";
+    [ [ "forall"; bl = binder_list; ","; c = operconstr LEVEL "200" ->
+          mkCProdN loc bl c
+      | "fun"; bl = binder_list; ty = type_cstr; "=>";
         c = operconstr LEVEL "200" ->
-          CLambdaN(loc,bl,mk_cast(c,ty))
-      | "let"; id=name; bl = LIST0 binder; ty = type_cstr; ":=";
-        c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
-          CLetIn(loc,id,mk_lam(bl,mk_cast(c1,ty)),c2)
-      | "let"; "("; lb = LIST1 name SEP ","; ")"; ":=";
+          mkCLambdaN loc bl (mk_cast(c,ty))
+      | "let"; id=name; bl = LIST0 binder_let; ty = type_cstr; ":=";
         c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
-          COrderedCase (loc, LetStyle, None, c1,
-                        [CLambdaN (loc, [lb, CHole loc], c2)])
+          let loc1 = match bl with
+            | LocalRawAssum ((loc,_)::_,_)::_ -> loc
+            | LocalRawDef ((loc,_),_)::_ -> loc
+            | _ -> dummy_loc in
+          CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2)
+      | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
+	  po = return_type;
+	  ":="; c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
+          CLetTuple (loc,List.map snd lb,po,c1,c2)
       | "if"; c1=operconstr; "then"; c2=operconstr LEVEL "200";
         "else"; c3=operconstr LEVEL "200" ->
           COrderedCase (loc, IfStyle, None, c1, [c2; c3])
@@ -205,7 +239,7 @@ GEXTEND Gram
         c=operconstr LEVEL "200" -> (loc,id,bl,ann,c,ty) ] ]
   ;
   fixannot:
-    [ [ "{"; "struct"; id=name; "}" -> Some id
+    [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
       | -> None ] ]
   ;
   match_constr:
@@ -213,14 +247,23 @@ GEXTEND Gram
         br=branches; "end" -> mk_match (loc,ci,ty,br) ] ]
   ;
   case_item:
-    [ [ c=operconstr LEVEL "80"; p=pred_pattern -> (c,p) ] ]
+    [ [ c=operconstr LEVEL "100"; p=pred_pattern -> 
+      match c,p with
+        | CRef (Ident (_,id)), (Names.Anonymous,x) -> (c,(Name id,x))
+        | _ -> (c,p) ] ]
   ;
   pred_pattern:
-    [ [ oid = OPT ["as"; id=name -> id];
-        (_,ty) = type_cstr -> (oid,ty) ] ]
+    [ [ oid = ["as"; id=name -> snd id | -> Names.Anonymous];
+        ty = OPT ["in"; r=global; nal=LIST0 name ->
+          (loc,r,List.map snd nal)] ->
+          (oid,ty) ] ]
   ;
   case_type:
-    [ [ ty = OPT [ "=>"; c = lconstr -> c ] -> ty ] ]
+    [ [ ty = OPT [ "return"; c = operconstr LEVEL "100" -> c ] -> ty ] ]
+  ;
+  return_type:
+    [ [ na = ["as"; id=name -> snd id | -> Names.Anonymous];
+        ty = case_type -> (na,ty) ] ]
   ;
   branches:
     [ [ OPT"|"; br=LIST0 eqn SEP "|" -> br ] ]
@@ -252,9 +295,25 @@ GEXTEND Gram
       | p1=pattern; ","; p2=lpattern ->  CPatCstr (loc, pair loc, [p1;p2]) ] ]
   ;
   binder_list:
-    [ [ idl=LIST1 name; bl=LIST0 binder -> (idl,CHole loc)::bl
-      | "("; idl=LIST1 name; ":"; c=lconstr; ")"; bl=LIST0 binder ->(idl,c)::bl
-      | idl=LIST1 name; ":"; c=constr -> [(idl,c)] ] ]
+    [ [ idl=LIST1 name; bl=LIST0 binder_let -> 
+          LocalRawAssum (idl,CHole loc)::bl
+      | idl=LIST1 name; ":"; c=lconstr -> 
+          [LocalRawAssum (idl,c)]
+      | "("; idl=LIST1 name; ":"; c=lconstr; ")"; bl=LIST0 binder_let ->
+          LocalRawAssum (idl,c)::bl ] ]
+  ;
+  binder_let:
+    [ [ id=name ->
+          LocalRawAssum ([id],CHole loc)
+      | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> 
+          LocalRawAssum (id::idl,c)
+      | "("; id=name; ":"; c=lconstr; ")" -> 
+          LocalRawAssum ([id],c)
+      | "("; id=name; ":="; c=lconstr; ")" ->
+          LocalRawDef (id,c)
+      | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> 
+          LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c,t))
+    ] ]
   ;
   binder:
     [ [ id=name -> ([id],CHole loc)
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 986e6b0589..ad78104cff 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -73,8 +73,8 @@ GEXTEND Gram
 
   tactic_expr:
     [ "5" LEFTA
-      [ ta0 = tactic_expr; "&"; ta1 = tactic_expr -> TacThen (ta0, ta1)
-      | ta = tactic_expr; "&"; "["; lta = LIST0 tactic_expr SEP "|"; "]" ->
+      [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
+      | ta = tactic_expr; ";"; "["; lta = LIST0 tactic_expr SEP "|"; "]" ->
           TacThens (ta, lta) ]
     | "4"
       [ ]
@@ -186,10 +186,12 @@ GEXTEND Gram
   ;
 
   (* Definitions for tactics *)
+(*
   deftok:
     [ [ IDENT "Meta"
       | IDENT "Tactic" ] ]
   ;
+*)
   tacdef_body:
     [ [ name = identref; it=LIST1 input_fun; ":="; body = tactic_expr ->
 	  (name, TacFun (it, body))
@@ -200,9 +202,7 @@ GEXTEND Gram
     [ [ tac = tactic_expr -> tac ] ]
   ;
   Vernac_.command: 
-    [ [ deftok; "Definition"; b = tacdef_body ->
-          VernacDeclareTacticDefinition (false, [b])
-      | IDENT "Recursive"; deftok; "Definition"; 
+    [ [ IDENT "Ltac";
         l = LIST1 tacdef_body SEP "with" ->
           VernacDeclareTacticDefinition (true, l) ] ]
   ;
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4
index de18ab7645..4ca29e2325 100644
--- a/parsing/g_primnew.ml4
+++ b/parsing/g_primnew.ml4
@@ -22,7 +22,7 @@ let _ =
   f Prim.ast;
   f Prim.reference
 
-let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'";"."]
+let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'"]
 let _ = List.iter (fun s -> Lexer.add_token("",s)) prim_kw
 
 ifdef Quotify then
@@ -83,7 +83,7 @@ GEXTEND Gram
     [ [ s = METAIDENT -> Nmeta (loc,s) ] ]
   ;
   field:
-    [ [ "."; s = IDENT -> local_id_of_string s ] ]
+    [ [ s = FIELD -> local_id_of_string s ] ]
   ;
   fields:
     [ [ id = field; (l,id') = fields -> (local_append l id,id')
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5b2e165ac2..0c9e0ce26c 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -124,11 +124,11 @@ GEXTEND Gram
     [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
          (dbnames, 
 	  HintsResolve
-	    (List.map (fun qid -> (None, CAppExpl(loc,(false,qid),[]))) l))
+	    (List.map (fun qid -> (None, CAppExpl(loc,(None,qid),[]))) l))
       | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases ->
         (dbnames, 
 	 HintsImmediate
-	   (List.map (fun qid-> (None, CAppExpl (loc,(false,qid),[]))) l))
+	   (List.map (fun qid-> (None, CAppExpl (loc,(None,qid),[]))) l))
       | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases ->
         (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ]
     ;
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index 82896099f8..e0e3744263 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -61,9 +61,8 @@ GEXTEND Gram
       | IDENT "Unfocus" -> VernacUnfocus
       | IDENT "Show" -> VernacShow (ShowGoal None)
       | IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n))
-      | IDENT "Show"; IDENT "Implicits"; n = natural ->
-	  VernacShow (ShowGoalImplicitly (Some n))
-      | IDENT "Show"; IDENT "Implicits" -> VernacShow (ShowGoalImplicitly None)
+      | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
+	  VernacShow (ShowGoalImplicitly n)
       | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
       | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript
       | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index bd71bbd5cf..017cfd18f0 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -135,7 +135,7 @@ GEXTEND Gram
 	  (Some (nl,c1), c2) ] ]
   ;
   pattern_occ:
-    [ [ nl = LIST0 integer; c = [c=constr->c | g=global->Topconstr.CRef g]-> (nl,c) ] ]
+    [ [ c = constr; nl = LIST0 integer -> (nl,c) ] ]
   ;
   pattern_occ_hyp_tail_list:
     [ [ pl = pattern_occ_hyp_list -> pl | -> (None,[]) ] ]
@@ -176,7 +176,7 @@ GEXTEND Gram
     [ [ "with"; bl = binding_list -> bl | -> NoBindings ] ]
   ;
   unfold_occ:
-    [ [ nl = LIST0 integer; c = global -> (nl,c) ] ]
+    [ [ c = global; nl = LIST0 integer -> (nl,c) ] ]
   ;
   red_flag:
     [ [ IDENT "beta" -> FBeta
@@ -194,9 +194,9 @@ GEXTEND Gram
       | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
       | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
-      | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
+      | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
-      | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl ] ]
+      | IDENT "pattern"; pl = LIST1 pattern_occ SEP "," -> Pattern pl ] ]
   ;
   (* This is [red_tactic] including possible extensions *)
   red_expr:
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0d431ea93b..d038e7d8c3 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -183,8 +183,8 @@ GEXTEND Gram
   ;
   gallina:
     (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = base_ident; bl = binders_list; ":"; c = constr ->
-         VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
+    [ [ thm = thm_token; id = base_ident; ":"; c = constr ->
+         VernacStartTheoremProof (thm, id, ([], c), false, (fun _ _ -> ()))
       | (f,d,e) = def_token; id = base_ident; b = def_body -> 
           VernacDefinition (d, id, b, f, e)
       | stre = assumption_token; bl = ne_params_list -> 
@@ -200,7 +200,7 @@ GEXTEND Gram
       | "CoInductive" -> false ] ]
   ;
   record_token:
-    [ [ IDENT "Record" -> () | IDENT "Structure" -> () ] ]
+    [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ]
   ;
   constructor:
     [ [ idl = LIST1 base_ident SEP ","; coe = of_type_with_opt_coercion;
@@ -305,10 +305,10 @@ GEXTEND Gram
         indl = block_old_style ->
 	  let indl' = List.map (fun (id,ar,c) -> (id,None,bl,ar,c)) indl in
 	  VernacInductive (f,indl')
-      | record_token; oc = opt_coercion; name = base_ident;
+      | b = record_token; oc = opt_coercion; name = base_ident;
 	ps = simple_binders_list; ":";
 	s = constr; ":="; c = rec_constructor; "{"; fs = fields; "}" ->
-	  VernacRecord ((oc,name),ps,s,c,fs)
+	  VernacRecord (b,(oc,name),ps,s,c,fs)
     ] ]
   ;
   gallina:
@@ -422,7 +422,7 @@ GEXTEND Gram
 	   let c = match n with
 	     | Some n ->
 		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
-		 CApp (loc,(false,c),l)
+		 CApp (loc,(None,c),l)
 	     | None -> c in
 	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 809ba58cfd..a9866b7e8b 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -42,13 +42,13 @@ let def_body = Gram.Entry.create "vernac:def_body"
 GEXTEND Gram
   GLOBAL: vernac gallina_ext;
   vernac:
-    (* Better to parse ";" here: in case of failure (e.g. in coerce_to_var), *)
-    (* ";" is still in the stream and discard_to_dot works correctly         *)
-    [ [ g = gallina; ";" -> g 
-      | g = gallina_ext; ";" -> g
-      | c = command; ";" -> c 
-      | c = syntax; ";" -> c
-      | "["; l = LIST1 located_vernac; "]"; ";" -> VernacList l
+    (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
+    (* "." is still in the stream and discard_to_dot works correctly         *)
+    [ [ g = gallina; "." -> g 
+      | g = gallina_ext; "." -> g
+      | c = command; "." -> c 
+      | c = syntax; "." -> c
+      | "["; l = LIST1 located_vernac; "]"; "." -> VernacList l
     ] ]
   ;
   vernac: FIRST
@@ -56,7 +56,7 @@ GEXTEND Gram
   ;
   vernac: LAST
     [ [ gln = OPT[n=natural; ":" -> n];
-        tac = subgoal_command; ";" -> tac gln ] ]
+        tac = subgoal_command; "." -> tac gln ] ]
   ;
   subgoal_command:
     [ [ c = check_command -> c
@@ -86,22 +86,27 @@ let no_coercion loc (c,x) =
     (loc,"no_coercion",Pp.str"no coercion allowed here");
   x
 
+let flatten_assum l =
+  List.flatten
+    (List.map (fun (oc,(idl,t)) -> List.map (fun id -> (oc,(id,t))) idl) l)
+
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
-    [ [ thm = thm_token; id = base_ident; bl = LIST0 binder; ":";
+    [ [ thm = thm_token; id = base_ident; (* bl = LIST0 binder; *) ":";
         c = lconstr ->
+          let bl = [] in
           VernacStartTheoremProof (thm, id, (bl, c), false, (fun _ _ -> ()))
       | (f,d,e) = def_token; id = base_ident; b = def_body -> 
           VernacDefinition (d, id, b, f, e)
-      | stre = assumption_token; bl = LIST1 simple_binder_coe -> 
-	  VernacAssumption (stre, bl)
-      | stre = assumptions_token; bl = LIST1 simple_binder_coe ->
+      | stre = assumption_token; bl = LIST1 assum_coe -> 
+	  VernacAssumption (stre, flatten_assum bl)
+      | stre = assumptions_token; bl = LIST1 assum_coe ->
 	  test_plurial_form bl;
-	  VernacAssumption (stre, bl)
+	  VernacAssumption (stre, flatten_assum bl)
       (* Gallina inductive declarations *)
       | (* Non port�� (?) : OPT[IDENT "Mutual"];*) f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
@@ -113,11 +118,11 @@ GEXTEND Gram
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l ] ]
   ;
   gallina_ext:
-    [ [ record_token; oc = opt_coercion; name = base_ident;
+    [ [ b = record_token; oc = opt_coercion; name = base_ident;
         ps = LIST0 simple_binder; ":";
 	s = lconstr; ":="; cstr = OPT base_ident; "{";
-        fs = LIST0 local_decl_expr; "}" ->
-	  VernacRecord ((oc,name),ps,s,cstr,fs)
+        fs = LIST0 record_field SEP ";"; "}" ->
+	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
 (* Non port�� ?
       | f = finite_token; s = csort; id = base_ident;
         indpar = LIST0 simple_binder; ":="; lc = constructor_list -> 
@@ -154,17 +159,17 @@ GEXTEND Gram
       | "CoInductive" -> false ] ]
   ;
   record_token:
-    [ [ IDENT "Record" -> () | IDENT "Structure" -> () ] ]
+    [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ]
   ;
   (* Simple definitions *)
   def_body:
-    [ [ bl = LIST0 binder; ":="; red = reduce; c = lconstr ->
+    [ [ bl = LIST0 binder_let; ":="; red = reduce; c = lconstr ->
       (match c with
           CCast(_,c,t) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
-      | bl = LIST0 binder; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
+      | bl = LIST0 binder_let; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
           DefineBody (bl, red, c, Some t)
-      | bl = LIST0 binder; ":"; t = lconstr ->
+      | bl = LIST0 binder_let; ":"; t = lconstr ->
           ProveBody (bl, t) ] ]
   ;
   reduce:
@@ -182,8 +187,8 @@ GEXTEND Gram
 	  (id,ntn,indpar,c,lc) ] ]
   ;
   constructor_list:
-    [ [ "|"; l = LIST1 constructor_binder SEP "|" -> l
-      | l = LIST1 constructor_binder SEP "|" -> l
+    [ [ "|"; l = LIST1 constructor SEP "|" -> l
+      | l = LIST1 constructor SEP "|" -> l
       |  -> [] ] ]
   ;
 (*
@@ -225,7 +230,7 @@ GEXTEND Gram
           (id,CProdN(loc,bl,c),CLambdaN(loc,bl,def)) ] ]
   ;
   rec_annotation:
-    [ [ "{"; "struct"; id=IDENT; "}" -> id_of_string id ] ]
+    [ [ "{"; IDENT "struct"; id=IDENT; "}" -> id_of_string id ] ]
   ;
   type_cstr:
     [ [ ":"; c=lconstr -> c 
@@ -246,17 +251,8 @@ GEXTEND Gram
   simple_binder:
     [ [ b = simple_binder_coe -> no_coercion loc b ] ]
   ;
-  binder:
-    [ [ na = name ->  LocalRawAssum([na],CHole loc)
-      | "("; na = name; ")" -> LocalRawAssum([na],CHole loc)
-      | "("; na = name; ":"; c = lconstr; ")"
-          -> LocalRawAssum([na],c)
-      | "("; na = name; ":="; c = lconstr; ")" ->
-          LocalRawDef (na,c)
-    ] ]
-  ;
   binder_nodef:
-    [ [ b = binder ->
+    [ [ b = binder_let ->
       (match b with
           LocalRawAssum(l,ty) -> (l,ty)
         | LocalRawDef _ ->
@@ -264,20 +260,21 @@ GEXTEND Gram
               (loc,"fix_param",Pp.str"defined binder not allowed here")) ] ]
   ;
   (* ... with coercions *)
-  local_decl_expr:
+  record_field:
     [ [ id = base_ident -> (false,AssumExpr(id,CHole loc))
-      | "("; id = base_ident; ")" -> (false,AssumExpr(id,CHole loc))
-      | "("; id = base_ident; oc = of_type_with_opt_coercion;
-             t = lconstr; ")" ->
+      | id = base_ident; oc = of_type_with_opt_coercion; t = lconstr ->
          (oc,AssumExpr (id,t))
-      | "("; id = base_ident; oc = of_type_with_opt_coercion;
-             t = lconstr; ":="; b = lconstr; ")" ->
-	 (oc,DefExpr (id,b,Some t))
-      | "("; id = base_ident; ":="; b = lconstr; ")" ->
+      | id = base_ident; oc = of_type_with_opt_coercion;
+             t = lconstr; ":="; b = lconstr -> (oc,DefExpr (id,b,Some t))
+      | id = base_ident; ":="; b = lconstr ->
          match b with
              CCast(_,b,t) -> (false,DefExpr(id,b,Some t))
            | _ -> (false,DefExpr(id,b,None)) ] ]
   ;
+  assum_coe:
+    [ [ "("; idl = LIST1 base_ident; oc = of_type_with_opt_coercion;
+        c = lconstr; ")" -> (oc,(idl,c)) ] ]
+  ;
   simple_binder_coe:
     [ [ id=base_ident -> (false,(id,CHole loc))
       | "("; id = base_ident; ")" -> (false,(id,CHole loc))
@@ -285,7 +282,7 @@ GEXTEND Gram
              t = lconstr; ")" ->
          (oc,(id,t)) ] ]
   ;
-  constructor_binder:
+  constructor:
     [ [ id = base_ident; coe = of_type_with_opt_coercion; c = lconstr ->
         (coe,(id,c)) ] ]
   ;
@@ -431,8 +428,10 @@ GEXTEND Gram
 	     | None -> c in
 	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
 *)
-      | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
-	  VernacDeclareImplicits (qid,Some l)
+      | IDENT "Implicit"; IDENT "Arguments"; qid = global; 
+           pos = OPT [ "["; l = LIST0 natural; "]" -> l ] ->
+	  VernacDeclareImplicits (qid,pos)
+
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
 
       | IDENT "Implicit"; ["Variable"; "Type" | IDENT "Variables"; "Type"];
@@ -598,8 +597,8 @@ GEXTEND Gram
       | IDENT "Scope"; s = IDENT -> PrintScope s ] ]
   ;
   class_rawexpr:
-    [ [ IDENT "FUNCLASS" -> FunClass
-      | IDENT "SORTCLASS" -> SortClass
+    [ [ IDENT "Funclass" -> FunClass
+      | IDENT "Sortclass" -> SortClass
       | qid = global -> RefClass qid ] ]
   ;
   locatable:
@@ -669,11 +668,11 @@ GEXTEND Gram
      | IDENT "Arguments"; IDENT "Scope"; qid = global;
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
 
-     | IDENT "Infix"; local = locality; a = entry_prec; n = OPT natural; 
+     | IDENT "Infix"; local = locality; (*a = entry_prec; n = OPT natural; *)
 	 op = STRING; p = global;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         let (a,n,b) = Metasyntax.interp_infix_modifiers a n modl in
+         let (a,n,b) = Metasyntax.interp_infix_modifiers None None modl in
          VernacInfix (local,a,n,op,p,b,None,sc)
      | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr;
 	   l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing]
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 5e27f9ca8c..5545f00778 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -309,7 +309,7 @@ let parse_226_tail tk = parser
 
 (* Parse what follows a dot *)
 let parse_after_dot bp c strm =
-  if !Options.v7 then 
+  if (* !Options.v7 *) true then 
     match strm with parser
 	 | [< ' ('_' | 'a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ->
 	     ("FIELD", get_buff len)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 39047e6880..476b3abd50 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -353,6 +353,8 @@ module Constr =
     let pattern = Gram.Entry.create "constr:pattern"
     let annot = Gram.Entry.create "constr:annot"
     let constr_pattern = gec_constr "constr_pattern"
+    let binder_let = Gram.Entry.create "constr:binder_list"
+    let tuple_constr = Gram.Entry.create "constr:tuple_constr"
   end
 
 module Module =
@@ -618,6 +620,11 @@ let get_constr_entry en =
         snd (get_entry (get_univ "constr") "binder_constr"),
         None,
         false
+    | ETConstr(250,()) when not !Options.v7 ->
+        weaken_entry Constr.tuple_constr,
+(*        snd (get_entry (get_univ "constr") "tuple_construple"),*)
+        None,
+        false
     | _ -> compute_entry true (fun (n,()) -> Some n) en
 
 (* This computes the name to give to a production knowing the name and
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7bf1d837d2..a591f57b26 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -138,6 +138,8 @@ module Constr :
     val pattern : cases_pattern_expr Gram.Entry.e
     val annot : constr_expr Gram.Entry.e
     val constr_pattern : constr_expr Gram.Entry.e
+    val binder_let : local_binder Gram.Entry.e
+    val tuple_constr : constr_expr Gram.Entry.e
   end
 
 module Module : 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 361e24647c..b3118f7e7b 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -203,13 +203,13 @@ let pr_eqn pr (_,patl,rhs) =
     str "=>" ++
     brk (1,1) ++ pr ltop rhs) ++ spc ()
 
-let pr_cases pr po tml eqns =
+let pr_cases pr (po,_) tml eqns =
   hov 0 (
     pr_annotation pr po ++
     hv 0 (
       hv 0 (
 	str "Cases" ++ brk (1,2) ++
-	prlist_with_sep spc (pr ltop) tml ++ spc() ++ str "of") ++ brk(1,2) ++
+	prlist_with_sep spc (fun (tm,_) -> pr ltop tm) tml ++ spc() ++ str "of") ++ brk(1,2) ++
       prlist_with_sep (fun () -> str "| ") (pr_eqn pr) eqns ++
       str "end"))
 
@@ -247,15 +247,10 @@ let rec pr inherited a =
       hv 1 (
 	hv 1 (str "[" ++ pr_let_binder pr (snd x) a ++ bll ++ str "]") ++
 	brk (0,1) ++ b), lletin
-  | CAppExpl (_,(true,f),l) ->
-      let a,l = list_sep_last l in
-      pr_proj pr pr_explapp a f l, lapp
-  | CAppExpl (_,(false,f),l) -> pr_explapp pr f l, lapp
-  | CApp (_,(true,a),l) ->
-      let c,l = list_sep_last l in
-      assert (snd c = None);
-      pr_proj pr pr_app (fst c) a l, lapp
-  | CApp (_,(false,a),l) -> pr_app pr a l, lapp
+  | CAppExpl (_,((* V7 don't know about projections *)_,f),l) ->
+      pr_explapp pr f l, lapp
+  | CApp (_,(_,a),l) ->
+      pr_app pr a l, lapp
   | CCases (_,po,tml,eqns) ->
       pr_cases pr po tml eqns, lcases
   | COrderedCase (_,IfStyle,po,c,[b1;b2]) ->
@@ -267,15 +262,9 @@ let rec pr inherited a =
 	  str "if " ++ pr ltop c ++ spc () ++
 	  hov 0 (str "then" ++ brk (1,1) ++ pr ltop b1) ++ spc () ++
 	  hov 0 (str "else" ++ brk (1,1) ++ pr ltop b2))), lif
-  | COrderedCase (_,LetStyle,po,c,[CLambdaN(_,[_,CHole _ as bd],b)]) ->
-      hov 0 (
-	pr_annotation pr po ++
-	hv 0 (
-          str "let" ++ brk (1,1) ++
-	  hov 0 (str "(" ++ pr_binder pr bd ++ str ")") ++
-	  str " =" ++ brk (1,2) ++
-	  pr ltop c ++ spc () ++
-	  str "in " ++ pr ltop b)), lletin
+  | CLetTuple (_,nal,(na,po),c,b) ->
+      error "Let tuple not supported in v7"
+
   | COrderedCase (_,(MatchStyle|RegularStyle as style),po,c,bl) ->
       hov 0 (
 	hov 0 (
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 697c788901..9326ff5382 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -194,8 +194,8 @@ let rec mlexpr_of_constr = function
   | Topconstr.CProdN (loc,l,a) -> <:expr< Topconstr.CProdN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
   | Topconstr.CLambdaN (loc,l,a) -> <:expr< Topconstr.CLambdaN $dloc$ $mlexpr_of_list (mlexpr_of_pair (mlexpr_of_list (mlexpr_of_pair (fun _ -> dloc) mlexpr_of_name)) mlexpr_of_constr) l$ $mlexpr_of_constr a$ >>
   | Topconstr.CLetIn (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
-  | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
-  | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >>
+  | Topconstr.CAppExpl (loc,a,l) -> <:expr< Topconstr.CAppExpl $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_reference a$ $mlexpr_of_list mlexpr_of_constr l$ >>
+  | Topconstr.CApp (loc,a,l) -> <:expr< Topconstr.CApp $dloc$ $mlexpr_of_pair (mlexpr_of_option mlexpr_of_int) mlexpr_of_constr a$ $mlexpr_of_list (mlexpr_of_pair mlexpr_of_constr (mlexpr_of_option mlexpr_of_int)) l$ >>
   | Topconstr.CCases (loc,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.COrderedCase (loc,_,_,_,_) -> failwith "mlexpr_of_constr: TODO"
   | Topconstr.CHole loc -> <:expr< Topconstr.CHole $dloc$ >>
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 9f09c14bec..9cc66a37fe 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -222,14 +222,15 @@ let rec ast_of_raw = function
       (* Pour compatibilit� des theories, il faut LAMBDALIST partout *)
       ope("LAMBDALIST",[ast_of_raw t;a])
 
-  | RCases (_,typopt,tml,eqns) ->
+  | RCases (_,(typopt,_),tml,eqns) ->
       let pred = ast_of_rawopt typopt in
       let tag = "CASES" in
-      let asttomatch = ope("TOMATCH", List.map ast_of_raw tml) in
+      let asttomatch =
+	ope("TOMATCH", List.map (fun (tm,_) -> ast_of_raw tm) tml) in
       let asteqns = List.map ast_of_eqn eqns in 
       ope(tag,pred::asttomatch::asteqns)
 	
-  | ROrderedCase (_,LetStyle,typopt,tm,[|bv|]) ->
+  | ROrderedCase (_,LetStyle,typopt,tm,[|bv|],_) ->
       let nvar' = function Anonymous -> nvar wildcard | Name id -> nvar id in
       let rec f l = function
         | RLambda (_,na,RHole _,c) -> f (nvar' na :: l) c
@@ -239,7 +240,7 @@ let rec ast_of_raw = function
       let eqn = ope ("EQN", [c;ope ("PATTCONSTRUCT",(nvar wildcard)::l)]) in
       ope ("FORCELET",[(ast_of_rawopt typopt);(ast_of_raw tm);eqn])
 
-  | ROrderedCase (_,st,typopt,tm,bv) ->
+  | ROrderedCase (_,st,typopt,tm,bv,_) ->
       let tag = match st with
 	| IfStyle -> "FORCEIF"
 	| RegularStyle -> "CASE"
@@ -250,6 +251,10 @@ let rec ast_of_raw = function
       ope(tag,(ast_of_rawopt typopt)
 	    ::(ast_of_raw tm)
 	    ::(Array.to_list (Array.map ast_of_raw bv)))
+
+  | RLetTuple (loc,nal,(na,typopt),tm,b) ->
+      error "Let tuple not supported in v7"
+
   | RRec (_,fk,idv,tyv,bv) ->
       let alfi = Array.map ast_of_ident idv in
       (match fk with