*** empty log message ***

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

3 files changed, 11 insertions, 7 deletions

diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index a39cfc4b55..c57e7761d0 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -136,7 +136,7 @@ GEXTEND Gram
 	  ConstrMayEval (ConstrEval (rtc,c))
       | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" ->
 	  ConstrMayEval (ConstrContext (id,c))
-      | IDENT "type"; "of"; c = Constr.constr ->
+      | IDENT "type"; IDENT "of"; c = Constr.constr ->
 	  ConstrMayEval (ConstrTypeOf c)
       | IDENT "fresh"; s = OPT STRING ->
 	  TacFreshId s ] ]
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 4975aed3cd..24f2be5817 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -134,7 +134,7 @@ GEXTEND Gram
     [ [ n = integer  -> Genarg.ArgArg n
       | id = identref -> Genarg.ArgVar id ] ]
   ;
-  autoarg_depth:
+(*  autoarg_depth:
   [ [ n = OPT natural -> n ] ]
   ;
   autoarg_adding:
@@ -144,12 +144,12 @@ GEXTEND Gram
   [ [ IDENT "destructing" -> true | -> false ] ]
   ;
   autoarg_usingTDB:
-  [ [ "using"; "tdb"  -> true | -> false ] ]
+  [ [ "using"; IDENT "tdb"  -> true | -> false ] ]
   ;
   autoargs:
   [ [ a0 = autoarg_depth; l = autoarg_adding; 
       a2 = autoarg_destructing; a3 = autoarg_usingTDB -> (a0,l,a2,a3) ] ]
-  ;
+  ;*)
   (* An identifier or a quotation meta-variable *)
   id_or_meta:
     [ [ id = identref -> AI id 
@@ -251,8 +251,10 @@ GEXTEND Gram
   ;
   hypident:
     [ [ id = id_or_meta -> id,(InHyp,ref None)
-      | "("; IDENT "type"; "of"; id = id_or_meta; ")" -> id,(InHypTypeOnly,ref None)
-      | "("; IDENT "value"; "of"; id = id_or_meta; ")" -> id,(InHypValueOnly,ref None)
+      | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" ->
+          id,(InHypTypeOnly,ref None)
+      | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" ->
+          id,(InHypValueOnly,ref None)
     ] ]
   ;
   hypident_occ:
@@ -371,11 +373,13 @@ GEXTEND Gram
       | IDENT "trivial"; db = hintbases -> TacTrivial db
       | IDENT "auto"; n = OPT natural; db = hintbases -> TacAuto (n, db)
 
+(* Obsolete since V8.0
       | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n
       | IDENT "cdhyp"; id = identref -> TacDestructHyp (true,id)
       | IDENT "dhyp";  id = identref -> TacDestructHyp (false,id)
       | IDENT "dconcl"  -> TacDestructConcl
       | IDENT "superauto"; l = autoargs -> TacSuperAuto l
+*)
       | IDENT "auto"; n = OPT natural; IDENT "decomp"; p = OPT natural ->
 	  TacDAuto (n, p)
 
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index eb41db74a8..8c0b6ef73d 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -110,7 +110,7 @@ GEXTEND Gram
 	  test_plurial_form l;
 	  VernacAssumption (stre, l)
       (* Gallina inductive declarations *)
-      | (* Non porté (?) : OPT[IDENT "Mutual"];*) f = finite_token;
+      | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
           VernacInductive (f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->