changement nouvelle syntaxe (pt fixes)

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

12 files changed, 177 insertions, 138 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 88c821167..6d1d317e6 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -55,7 +55,6 @@ let default_levels_v8 =
   [200,Gramext.RightA;
    100,Gramext.RightA;
    80,Gramext.RightA;
-   40,Gramext.LeftA;
    10,Gramext.LeftA;
    9,Gramext.RightA;
    1,Gramext.LeftA;
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index e8f9c38c5..ce45d73b0 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -22,7 +22,7 @@ open Util
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
     "end"; "as"; "let"; "if"; "then"; "else"; "return";
-    "Prop"; "Set"; "Type"; ".(" ]
+    "Prop"; "Set"; "Type"; ".("; "_" ]
 
 let _ = 
   if not !Options.v7 then
@@ -46,47 +46,20 @@ let mk_lam = function
     ([],c) -> c
   | (bl,c) -> CLambdaN(constr_loc c, bl,c)
 
-let coerce_to_id c =
-  match c with
-      CRef(Ident(loc,id)) -> (loc,Name id)
-    | CHole loc -> (loc,Anonymous)
-    | _ -> error "ill-formed match type annotation"
-
-let match_bind_of_pat loc (oid,ty) =
-  let l2 =
-    match oid with
-        None -> []
-      | Some x -> [([x],CHole loc)] in
-  let l1 =
-    match ty with
-        None -> [] (* No: should lookup inductive arity! *)
-      | Some (CApp(_,_,args)) -> (* parameters do not appear *)
-          List.map (fun (c,_) -> ([coerce_to_id c],CHole loc)) args
-      | _ -> error "ill-formed match type annotation" in
-  l1@l2
-
 let mk_match (loc,cil,rty,br) =
-(*
-  let (lc,pargs) = List.split cil in
-  let pr =
-    match rty with
-        None -> None
-      | Some ty ->
-          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,(None,rty),cil,br)
 
+let index_of_annot bl ann =
+  match bl,ann with
+      [([_],_)], None -> 0
+    | _, Some x ->
+        let ids = List.map snd (List.flatten (List.map fst bl)) in
+        (try list_index (snd x) ids - 1
+        with Not_found -> error "no such fix variable")
+    | _ -> error "cannot guess decreasing argument of fix"
+
 let mk_fixb (loc,id,bl,ann,body,(tloc,tyc)) =
-  let n =
-    match bl,ann with
-        [([_],_)], None -> 0
-      | _, Some x ->
-          let ids = List.map snd (List.flatten (List.map fst bl)) in
-          (try list_index (snd x) ids - 1
-          with Not_found -> error "no such fix variable")
-      | _ -> error "cannot find decreasing arg of fix" in
+  let n = index_of_annot bl ann in
   let ty = match tyc with
       None -> CHole tloc
     | Some t -> CProdN(loc,bl,t) in
@@ -113,7 +86,6 @@ 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 -> 
@@ -132,33 +104,35 @@ let rec mkCLambdaN loc bll c =
   | [] -> c
   | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
 
-(* Hack to parse "(n)" as nat without conflicts with the (useless) *)
-(* admissible notation "(n)" *)
-let test_lpar_id_coloneq =
+(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
+(* admissible notation "(x t)" *)
+let lpar_id_coloneq =
   Gram.Entry.of_parser "test_lpar_id_coloneq"
     (fun strm ->
-      match Stream.npeek 1 strm with
-        | [("", "(")] ->
-            begin match Stream.npeek 2 strm with
-              | [_; ("IDENT", _)] ->
-		  begin match Stream.npeek 3 strm with
-		    | [_; _; ("", ":=")] -> ()
-		    | _ -> raise Stream.Failure
-		  end
-	      | _ -> raise Stream.Failure
-            end
-        | _ -> raise Stream.Failure)
+      match Stream.npeek 3 strm with
+	| [("","("); ("IDENT",s); ("", ":=")] ->
+            Stream.junk strm; Stream.junk strm; Stream.junk strm;
+            Names.id_of_string s
+	| _ -> raise Stream.Failure);;
+
 
 if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
-  constr_pattern lconstr_pattern Constr.ident binder_let tuple_constr;
+  constr_pattern lconstr_pattern Constr.ident binder binder_let
+  tuple_constr;
   Constr.ident:
     [ [ id = Prim.ident -> id
 
       (* This is used in quotations and Syntax *)
       | id = METAIDENT -> id_of_string id ] ]
   ;
+  Prim.name:
+    [ [ "_" -> (loc, Anonymous) ] ]
+  ;
+  Prim.ast:
+    [ [ "_" -> Coqast.Nvar(loc,id_of_string"_") ] ]
+  ;
   global:
     [ [ r = Prim.reference -> r
 
@@ -177,7 +151,7 @@ GEXTEND Gram
       | "Type" -> RType None ] ]
   ;
   lconstr:
-    [ [ c = operconstr -> c ] ]
+    [ [ c = operconstr LEVEL "200" -> c ] ]
   ;
   constr:
     [ [ c = operconstr LEVEL "9" -> c ] ]
@@ -197,8 +171,6 @@ GEXTEND Gram
     | "80" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
       | c1 = operconstr; "->"; c2 = operconstr    -> CArrow(loc,c1,c2) ]
-    | "40L" LEFTA
-      [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ]
     | "10L" LEFTA
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
       | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
@@ -206,7 +178,8 @@ GEXTEND Gram
     | "1L" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
 	CApp(loc,(Some (List.length args+1),CRef f),args@[c,None])
-      | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT; ")" ->
+      | c=operconstr; ".("; "@"; f=global;
+        args=LIST0 (operconstr LEVEL "9"); ")" ->
         CAppExpl(loc,(Some (List.length args+1),f),args@[c]) 
       | c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ]
     | "0"
@@ -217,19 +190,25 @@ GEXTEND Gram
   binder_constr:
     [ [ "forall"; bl = binder_list; ","; c = operconstr LEVEL "200" ->
           mkCProdN loc bl c
-      | "fun"; bl = binder_list; ty = type_cstr; "=>";
-        c = operconstr LEVEL "200" ->
-          mkCLambdaN loc bl (mk_cast(c,ty))
+      | "fun"; bl = binder_list; "=>"; c = operconstr LEVEL "200" ->
+          mkCLambdaN loc bl c
       | "let"; id=name; bl = LIST0 binder_let; ty = type_cstr; ":=";
-        c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
+        c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" ->
           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"; fx = fix_constr; "in"; c = operconstr LEVEL "200" ->
+          let (li,id) = match fx with
+              CFix(_,id,_) -> id
+            | CCoFix(_,id,_) -> id
+            | _ -> assert false in
+          CLetIn(loc,(li,Name id),fx,c)
       | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []];
 	  po = return_type;
-	  ":="; c1 = operconstr; "in"; c2 = operconstr LEVEL "200" ->
+	  ":="; c1 = operconstr LEVEL "200"; "in";
+          c2 = operconstr LEVEL "200" ->
           CLetTuple (loc,List.map snd lb,po,c1,c2)
       | "if"; c=operconstr; po = return_type;
 	"then"; b1=operconstr LEVEL "200";
@@ -238,21 +217,15 @@ GEXTEND Gram
       | c=fix_constr -> c ] ]
   ;
   appl_arg:
-    [ [ _ = test_lpar_id_coloneq; "("; id = ident; ":="; c=lconstr; ")" ->
+    [ [ id = lpar_id_coloneq; c=lconstr; ")" ->
 	  (c,Some (loc,ExplByName id))
-(*
-      | "@"; n=INT; ":="; c=constr -> (c,Some(loc,ExplByPos (int_of_string n)))
-*)
       | c=constr -> (c,None) ] ]
   ;
   atomic_constr:
     [ [ g=global -> CRef g
       | s=sort -> CSort(loc,s)
       | n=INT -> CNumeral (loc,Bignat.POS (Bignat.of_string n))
-      | IDENT "_" -> CHole loc
-(*
-      | "?"; n=Prim.natural -> CPatVar(loc,(false,Pattern.patvar_of_int n)) ] ]
-*)
+      | "_" -> CHole loc
       | "?"; id=ident -> CPatVar(loc,(false,id)) ] ]
   ;
   fix_constr:
@@ -282,12 +255,13 @@ GEXTEND Gram
   case_item:
     [ [ c=operconstr LEVEL "100"; p=pred_pattern -> 
       match c,p with
-        | CRef (Ident (_,id)), (Names.Anonymous,x) -> (c,(Name id,x))
-        | _ -> (c,p) ] ]
+        | CRef (Ident (_,id)), (None,indp) -> (c,(Name id,indp))
+        | _, (None,indp) -> (c,(Anonymous,indp))
+        | _, (Some na,indp) -> (c,(na,indp)) ] ]
   ;
   pred_pattern:
-    [ [ oid = ["as"; id=name -> snd id | -> Names.Anonymous];
-        ty = OPT ["in"; t=lconstr -> t] -> (oid,ty) ] ]
+    [ [ ona = OPT ["as"; id=name -> snd id];
+        ty = OPT ["in"; t=lconstr -> t] -> (ona,ty) ] ]
   ;
   case_type:
     [ [ ty = OPT [ "return"; c = operconstr LEVEL "100" -> c ] -> ty ] ]
@@ -302,24 +276,23 @@ GEXTEND Gram
   eqn:
     [ [ pl = LIST1 pattern SEP ","; "=>"; rhs = lconstr -> (loc,pl,rhs) ] ]
   ;
-  simple_pattern:
-    [ [ r = Prim.reference -> CPatAtom (loc,Some r)
-      | IDENT "_" -> CPatAtom (loc,None)
-      | "("; p = lpattern; ")" -> p
-      | n = bigint -> CPatNumeral (loc,n)
-    ] ]
-  ;
   pattern:
-    [ [ p = pattern ; lp = LIST1 simple_pattern ->
+    [ "1" LEFTA
+      [ p = pattern ; lp = LIST1 (pattern LEVEL "0") ->
         (match p with
           | CPatAtom (_, Some r) -> CPatCstr (loc, r, lp)
           | _ -> Util.user_err_loc 
-              (loc, "compound_pattern", Pp.str "Constructor expected"))
+              (cases_pattern_loc p, "compound_pattern",
+               Pp.str "Constructor expected"))
       | p = pattern; "as"; id = base_ident ->
 	  CPatAlias (loc, p, id)
       | c = pattern; "%"; key=IDENT -> 
-          CPatDelimiters (loc,key,c)
-      | p = simple_pattern -> p ] ]
+          CPatDelimiters (loc,key,c) ]
+    | "0"
+      [ r = Prim.reference -> CPatAtom (loc,Some r)
+      | "_" -> CPatAtom (loc,None)
+      | "("; p = lpattern; ")" -> p
+      | n = bigint -> CPatNumeral (loc,n) ] ]
   ;
   lpattern:
     [ [ c = pattern -> c
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index 672aeb3b6..9d8dea149 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -142,7 +142,7 @@ GEXTEND Gram
       | "()" -> TacVoid ] ]
   ;
   input_fun:
-    [ [ IDENT "_" -> None 
+    [ [ "_" -> None 
       | l = base_ident -> Some l ] ]
   ;
   let_clause:
@@ -171,7 +171,7 @@ GEXTEND Gram
   match_context_rule:
     [ [ "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; "]";
         "=>"; te = tactic_expr -> Pat (largs, mp, te)
-      | IDENT "_"; "=>"; te = tactic_expr -> All te ] ]
+      | "_"; "=>"; te = tactic_expr -> All te ] ]
   ;
   match_context_list:
     [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl
@@ -179,7 +179,7 @@ GEXTEND Gram
   ;
   match_rule:
     [ [ "["; mp = match_pattern; "]"; "=>"; te = tactic_expr -> Pat ([],mp,te)
-      | IDENT "_"; "=>"; te = tactic_expr -> All te ] ]
+      | "_"; "=>"; te = tactic_expr -> All te ] ]
   ;
   match_list:
     [ [ mrl = LIST1 match_rule SEP "|" -> mrl
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 39a7687f1..7a1b910c6 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -88,7 +88,8 @@ GEXTEND Gram
     [ [ s = IDENT -> local_id_of_string s ] ]
   ;
   name:
-    [ [ IDENT "_" -> (loc, Anonymous) | id = base_ident -> (loc, Name id) ] ]
+    [ [ IDENT "_" -> (loc, Anonymous)
+      | id = base_ident -> (loc, Name id) ] ]
   ;
   identref:
     [ [ id = base_ident -> (loc,id) ] ]
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 18422b460..6c8ad0c1b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -295,12 +295,12 @@ GEXTEND Gram
       | IDENT "LApply"; c = constr -> TacLApply c
 
       (* Derived basic tactics *)
-      | IDENT "Induction"; h = quantified_hypothesis -> TacOldInduction h
+      | IDENT "Induction"; h = quantified_hypothesis -> TacSimpleInduction h
       | IDENT "NewInduction"; c = induction_arg; el = OPT eliminator;
           ids = with_names -> TacNewInduction (c,el,ids)
       | IDENT "Double"; IDENT "Induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
-      | IDENT "Destruct"; h = quantified_hypothesis -> TacOldDestruct h
+      | IDENT "Destruct"; h = quantified_hypothesis -> TacSimpleDestruct h
       | IDENT "NewDestruct"; c = induction_arg; el = OPT eliminator; 
           ids = with_names -> TacNewDestruct (c,el,ids)
       | IDENT "Decompose"; IDENT "Record" ; c = constr -> TacDecomposeAnd c
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 414311b0f..b17907844 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -22,17 +22,33 @@ let _ =
   if not !Options.v7 then
     List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
 
-(* Hack to parse "with n := c ..." as a binder without conflicts with the *)
-(* admissible notation "with c1 c2..." *)
-let test_lparcoloneq2 =
-  Gram.Entry.of_parser "test_lparcoloneq2"
+(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
+(* admissible notation "(x t)" *)
+let lpar_id_coloneq =
+  Gram.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
-      match Stream.npeek 1 strm with
-        | [("", "(")] ->
-            begin match Stream.npeek 3 strm with
-              | [_; _; ("", ":=")] -> ()
-              | _ -> raise Stream.Failure
-            end
+      match Stream.npeek 3 strm with
+	| [("","("); ("IDENT",s); ("", ":=")] ->
+            Stream.junk strm; Stream.junk strm; Stream.junk strm;
+            Names.id_of_string s
+	| _ -> raise Stream.Failure)
+
+(* idem for (x:=t) and (1:=t) *)
+let test_lpar_idnum_coloneq =
+  Gram.Entry.of_parser "test_lpar_idnum_coloneq"
+    (fun strm ->
+      match Stream.npeek 3 strm with
+        | [("","("); (("IDENT"|"INT"),_); ("", ":=")] -> ()
+        | _ -> raise Stream.Failure)
+
+(* idem for (x:t) *)
+let lpar_id_colon =
+  Gram.Entry.of_parser "test_lpar_id_colon"
+    (fun strm ->
+      match Stream.npeek 3 strm with
+        | [("","("); ("IDENT",id); ("", ":")] ->
+            Stream.junk strm; Stream.junk strm; Stream.junk strm;
+            Names.id_of_string id
         | _ -> raise Stream.Failure)
 
 (* open grammar entries, possibly in quotified form *)
@@ -42,10 +58,28 @@ open Constr
 open Prim
 open Tactic
 
-(* Functions overloaded by quotifier *)
+let mk_fix_tac (loc,id,bl,ann,ty) =
+  let n =
+    match bl,ann with
+        [([_],_)], None -> 0
+      | _, Some x ->
+          let ids = List.map snd (List.flatten (List.map fst bl)) in
+          (try list_index (snd x) ids
+          with Not_found -> error "no such fix variable")
+      | _ -> error "cannot guess decreasing argument of fix" in
+  (id,n,Topconstr.CProdN(loc,bl,ty))
 
+let mk_cofix_tac (loc,id,bl,ann,ty) =
+  let _ = option_app (fun (aloc,_) ->
+    Util.user_err_loc
+      (aloc,"Constr:mk_cofix_tac",
+       Pp.str"Annotation forbidden in cofix expression")) ann in
+  (id,Topconstr.CProdN(loc,bl,ty))
+
+(* Functions overloaded by quotifier *)
 let induction_arg_of_constr c =
-  try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c) with _ -> ElimOnConstr c
+  try ElimOnIdent (Topconstr.constr_loc c,coerce_to_id c)
+  with _ -> ElimOnConstr c
 
 let local_compute = [FBeta;FIota;FDeltaBut [];FZeta]
 
@@ -160,7 +194,7 @@ GEXTEND Gram
   simple_intropattern:
     [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc
       | "("; tc = LIST1 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc]
-      | IDENT "_" -> IntroWildcard
+      | "_" -> IntroWildcard
       | id = base_ident -> IntroIdentifier id
       ] ]
   ;
@@ -169,7 +203,8 @@ GEXTEND Gram
       | "("; n = natural; ":="; c = lconstr; ")" -> (loc, AnonHyp n, c) ] ]
   ;
   binding_list:
-    [ [ test_lparcoloneq2; bl = LIST1 simple_binding -> ExplicitBindings bl
+    [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding ->
+          ExplicitBindings bl
       | bl = LIST1 constr -> ImplicitBindings bl ] ]
   ;
   constr_with_bindings:
@@ -223,10 +258,12 @@ GEXTEND Gram
       | -> [] ] ]
   ;
   fixdecl:
-    [ [ id = base_ident; "/"; n = natural; ":"; c = constr -> (id,n,c) ] ]
+    [ [ id = base_ident; bl=LIST0 Constr.binder; ann=fixannot;
+        ":"; ty=lconstr -> (loc,id,bl,ann,ty) ] ]
   ;
-  cofixdecl:
-    [ [ id = base_ident; ":"; c = constr -> (id,c) ] ]
+  fixannot:
+    [ [ "{"; IDENT "struct"; id=name; "}" -> Some id
+      | -> None ] ]
   ;
   hintbases:
     [ [ "with"; "*" -> None
@@ -265,39 +302,42 @@ GEXTEND Gram
       | "fix"; n = natural -> TacFix (None,n)
       | "fix"; id = base_ident; n = natural -> TacFix (Some id,n)
       | "fix"; id = base_ident; n = natural; "with"; fd = LIST0 fixdecl ->
-	  TacMutualFix (id,n,fd)
+	  TacMutualFix (id,n,List.map mk_fix_tac fd)
       | "cofix" -> TacCofix None
       | "cofix"; id = base_ident -> TacCofix (Some id)
-      | "cofix"; id = base_ident; "with"; fd = LIST0 cofixdecl ->
-	  TacMutualCofix (id,fd)
+      | "cofix"; id = base_ident; "with"; fd = LIST0 fixdecl ->
+	  TacMutualCofix (id,List.map mk_cofix_tac fd)
 
       | IDENT "cut"; c = constr -> TacCut c
+      | IDENT "assert"; id = lpar_id_colon; t = lconstr; ")" ->
+          TacTrueCut (Some id,t)
+      | IDENT "assert"; id = lpar_id_coloneq; b = lconstr; ")" ->
+          TacForward (false,Names.Name id,b)
       | IDENT "assert"; c = constr -> TacTrueCut (None,c)
-      | IDENT "assert"; c = constr; ":"; t = lconstr ->
-          TacTrueCut (Some (coerce_to_id c),t)
-      | IDENT "assert"; c = constr; ":="; b = lconstr ->
-          TacForward (false,Names.Name (coerce_to_id c),b)
-      | IDENT "pose"; c = constr; ":="; b = lconstr ->
-	  TacForward (true,Names.Name (coerce_to_id c),b)
+      | IDENT "pose"; id = lpar_id_coloneq; b = lconstr; ")" ->
+	  TacForward (true,Names.Name id,b)
       | IDENT "pose"; b = constr -> TacForward (true,Names.Anonymous,b)
       | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc
       | IDENT "generalize"; IDENT "dependent"; c = constr ->
           TacGeneralizeDep c
-      | IDENT "lettac"; id = base_ident; ":="; c = lconstr; p = clause_pattern
-        -> TacLetTac (id,c,p)
-      | IDENT "instantiate"; n = natural; c = constr -> TacInstantiate (n,c)
+      | IDENT "lettac"; "("; id = base_ident; ":="; c = lconstr; ")";
+          p = clause_pattern -> TacLetTac (id,c,p)
+      | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")" ->
+          TacInstantiate (n,c)
 
       | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
 	  TacSpecialize (n,lcb)
       | IDENT "lapply"; c = constr -> TacLApply c
 
       (* Derived basic tactics *)
-      | IDENT "oldinduction"; h = quantified_hypothesis -> TacOldInduction h
+      | IDENT "simple_induction"; h = quantified_hypothesis ->
+          TacSimpleInduction h
       | IDENT "induction"; c = induction_arg; el = OPT eliminator;
           ids = with_names -> TacNewInduction (c,el,ids)
       | IDENT "double"; IDENT "induction"; h1 = quantified_hypothesis;
 	  h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2)
-      | IDENT "olddestruct"; h = quantified_hypothesis -> TacOldDestruct h
+      | IDENT "simple_destruct"; h = quantified_hypothesis ->
+          TacSimpleDestruct h
       | IDENT "destruct"; c = induction_arg; el = OPT eliminator; 
           ids = with_names -> TacNewDestruct (c,el,ids)
       | IDENT "decompose"; IDENT "record" ; c = constr -> TacDecomposeAnd c
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 8e0088890..28c0f5fd4 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -759,7 +759,7 @@ GEXTEND Gram
     ] ]
   ;
   opt_scope:
-    [ [ IDENT "_" -> None | sc = IDENT -> Some sc ] ]
+    [ [ "_" -> None | sc = IDENT -> Some sc ] ]
   ;
   (* Syntax entries for Grammar. Only grammar_entry is exported *)
   grammar_entry:
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 843bd068f..a96237e5b 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -110,7 +110,8 @@ let is_normal_token str =
   if String.length str > 0 then
     match str.[0] with
       | ' ' | '\n' | '\r' | '\t' | '"' -> bad_token str
-      | '_' | '$' | 'a'..'z' | 'A'..'Z' -> true
+      | '$' | 'a'..'z' | 'A'..'Z' -> true
+      | '_' -> !Options.v7
 	  (* utf-8 symbols of the form "E2 xx xx" [E2=226] *)
       | '\226' when String.length str > 2 ->
 	  (match str.[1], str.[2] with
@@ -122,9 +123,9 @@ let is_normal_token str =
 		false
 	    | _ ->
 		(* default to iso 8859-1 "â" *)
-		true)
+		!Options.v7)
 	  (* iso 8859-1 accentuated letters *)
-      | '\192'..'\214' | '\216'..'\246' | '\248'..'\255' -> true
+      | '\192'..'\214' | '\216'..'\246' | '\248'..'\255' -> !Options.v7
       | _ -> false
   else 
     bad_token str
@@ -347,7 +348,7 @@ let parse_226_tail tk = parser
 
 (* Parse what follows a dot *)
 let parse_after_dot bp c strm =
-  if (* !Options.v7 *) true then 
+  if !Options.v7 then 
     match strm with parser
 	 | [< ' ('_' | 'a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ->
 	     ("FIELD", get_buff len)
@@ -369,6 +370,19 @@ let parse_after_dot bp c strm =
 	 | [< (t,_) = process_chars bp c >] -> t
   else
     match strm with parser
+	 | [< ' ('a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ->
+	     ("FIELD", get_buff len)
+	 (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
+	 | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2); 
+	   len = ident (store (store 0 c1) c2) >] ->
+	     ("FIELD", get_buff len)
+         (* utf-8 mathematical symbols have format E2 xx xx [E2=226] *)
+	 | [< ''\226' as c1; t = parse_226_tail 
+	     (progress_special '.' (Some !token_tree)) >] ep ->
+	     (match t with
+	       | TokSymbol (Some t) -> ("", t)
+	       | TokSymbol None -> err (bp, ep) Undefined_token
+	       | TokIdent t -> ("FIELD", t))
 	 | [< (t,_) = process_chars bp c >] -> t
 
 
@@ -384,10 +398,20 @@ let rec next_token = parser bp
       comment_stop bp;
       if !Options.v7 & t=("",".") then between_com := true;
       (t, (bp,ep))
-  | [< ' ('_' | 'a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ep ->
+  | [< ' ('a'..'z' | 'A'..'Z' as c); len = ident (store 0 c) >] ep ->
       let id = get_buff len in 
       comment_stop bp;
       (try ("", find_keyword id) with Not_found -> ("IDENT", id)), (bp, ep)
+  | [< ''_' as c; s >] ->
+      if !Options.v7 then 
+        (match s with parser [< len = ident (store 0 c) >] ep ->
+          let id = get_buff len in 
+          comment_stop bp;
+          (try ("", find_keyword id) with Not_found -> ("IDENT", id)),
+          (bp, ep))
+      else
+        (match s with parser [< t = process_chars bp c >] ->
+          comment_stop bp; t)
   (* Greek utf-8 letters [CE80-CEBF and CF80-CFBF] (CE=206; BF=191) *)
   | [< ' ('\206' | '\207' as c1); ' ('\128'..'\191' as c2); 
 	   len = ident (store (store 0 c1) c2) >] ep ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 9bb2a86b9..1f462b615 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -348,7 +348,8 @@ module Constr =
     let annot = Gram.Entry.create "constr:annot"
     let constr_pattern = gec_constr "constr_pattern"
     let lconstr_pattern = gec_constr "lconstr_pattern"
-    let binder_let = Gram.Entry.create "constr:binder_list"
+    let binder = Gram.Entry.create "constr:binder"
+    let binder_let = Gram.Entry.create "constr:binder_let"
     let tuple_constr = gec_constr "tuple_constr"
   end
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 8f393030e..1c7a1932f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -139,6 +139,7 @@ module Constr :
     val annot : constr_expr Gram.Entry.e
     val constr_pattern : constr_expr Gram.Entry.e
     val lconstr_pattern : constr_expr Gram.Entry.e
+    val binder : (name located list * constr_expr) Gram.Entry.e
     val binder_let : local_binder Gram.Entry.e
     val tuple_constr : constr_expr Gram.Entry.e
   end
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d24de5675..166db8675 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -411,7 +411,7 @@ and pr_atom1 = function
   | TacCaseType c -> hov 1 (str "CaseType" ++ pr_arg pr_constr c)
   | TacFix (ido,n) -> hov 1 (str "Fix" ++ pr_opt pr_id ido ++ pr_intarg n)
   | TacMutualFix (id,n,l) ->
-      hov 1 (str "Cofix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
+      hov 1 (str "Fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc () ++
         hov 0 (str "with" ++ brk (1,1) ++
           prlist_with_sep spc
 	    (fun (id,n,c) ->
@@ -444,12 +444,12 @@ and pr_atom1 = function
       hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c)
 
   (* Derived basic tactics *)
-  | TacOldInduction h ->
+  | TacSimpleInduction h ->
       hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewInduction (h,e,ids) ->
       hov 1 (str "NewInduction" ++ spc () ++ pr_induction_arg pr_constr h ++
         pr_opt pr_eliminator e ++ pr_with_names ids)
-  | TacOldDestruct h ->
+  | TacSimpleDestruct h ->
       hov 1 (str "Destruct" ++ pr_arg pr_quantified_hypothesis h)
   | TacNewDestruct (h,e,ids) ->
       hov 1 (str "NewDestruct" ++ spc () ++ pr_induction_arg pr_constr h ++
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 6b89169b5..44e78462f 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -376,14 +376,14 @@ let rec mlexpr_of_atomic_tactic = function
       <:expr< Tacexpr.TacLetTac $id$ $mlexpr_of_constr c$ $cl$ >>
 
   (* Derived basic tactics *)
-  | Tacexpr.TacOldInduction h ->
-      <:expr< Tacexpr.TacOldInduction $mlexpr_of_quantified_hypothesis h$ >>
+  | Tacexpr.TacSimpleInduction h ->
+      <:expr< Tacexpr.TacSimpleInduction $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacNewInduction (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
       let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in
       <:expr< Tacexpr.TacNewInduction $mlexpr_of_induction_arg c$ $cbo$ $ids$>>
-  | Tacexpr.TacOldDestruct h ->
-      <:expr< Tacexpr.TacOldDestruct $mlexpr_of_quantified_hypothesis h$ >>
+  | Tacexpr.TacSimpleDestruct h ->
+      <:expr< Tacexpr.TacSimpleDestruct $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacNewDestruct (c,cbo,ids) ->
       let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in
       let ids = mlexpr_of_list (mlexpr_of_list mlexpr_of_intro_pattern) ids in