Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

16 files changed, 297 insertions, 208 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 3266fcf9..f554522a 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -107,6 +107,64 @@ let rec make_wit loc = function
         value wit = $lid:"wit_"^s$;
       end in WIT.wit >>
 
+let has_extraarg =
+  List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
+
+let statically_known_possibly_empty s (prods,_) =
+  List.for_all (function
+    | GramNonTerminal(_,ExtraArgType s',_,_) ->
+        (* For ExtraArg we don't know (we'll have to test dynamically) *)
+        (* unless it is a recursive call *)
+        s <> s'
+    | GramNonTerminal(_,(OptArgType _|List0ArgType _),_,_) ->
+        (* Opt and List0 parses the empty string *)
+        true
+    | _ ->
+        (* This consumes a token for sure *) false)
+      prods
+
+let possibly_empty_subentries loc (prods,act) =
+  let bind_name p v e = match p with
+    | None -> e
+    | Some id ->
+        let s = Names.string_of_id id in <:expr< let $lid:s$ = $v$ in $e$ >> in
+  let rec aux = function
+    | [] -> <:expr< let loc = $default_loc$ in let _ = loc = loc in $act$ >>
+    | GramNonTerminal(_,OptArgType _,_,p) :: tl ->
+        bind_name p <:expr< None >> (aux tl)
+    | GramNonTerminal(_,List0ArgType _,_,p) :: tl ->
+        bind_name p <:expr< [] >> (aux tl)
+    | GramNonTerminal(_,(ExtraArgType _ as t),_,p) :: tl ->
+        (* We check at runtime if extraarg s parses "epsilon" *)
+        let s = match p with None -> "_" | Some id -> Names.string_of_id id in
+        <:expr< let $lid:s$ = match Genarg.default_empty_value $make_rawwit loc t$ with
+          [ None -> raise Exit
+          | Some v -> v ] in $aux tl$ >>
+    | _ -> assert false (* already filtered out *) in
+  if has_extraarg prods then
+    (* Needs a dynamic check; catch all exceptions if ever some rhs raises *)
+    (* an exception rather than returning a value; *)
+    (* declares loc because some code can refer to it; *)
+    (* ensures loc is used to avoid "unused variable" warning *)
+    (true, <:expr< try Some $aux prods$ with [ _ -> None ] >>)
+  else
+    (* Static optimisation *)
+    (false, aux prods)
+
+let make_possibly_empty_subentries loc s cl =
+  let cl = List.filter (statically_known_possibly_empty s) cl in
+  if cl = [] then
+    <:expr< None >>
+  else
+    let rec aux = function
+    | (true, e) :: l ->
+        <:expr< match $e$ with [ Some v -> Some v | None -> $aux l$ ] >>
+    | (false, e) :: _ ->
+        <:expr< Some $e$ >>
+    | [] ->
+        <:expr< None >> in
+    aux (List.map (possibly_empty_subentries loc) cl)
+
 let make_act loc act pil =
   let rec make = function
     | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >>
@@ -144,9 +202,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let interp = match f with
     | None ->
 	<:expr< fun ist gl x ->
-          out_gen $make_wit loc globtyp$
-            (Tacinterp.interp_genarg ist gl
-               (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
+	  let (sigma,a_interp) =
+	    Tacinterp.interp_genarg ist gl
+               (Genarg.in_gen $make_globwit loc globtyp$ x)
+	  in
+          (sigma , out_gen $make_wit loc globtyp$ a_interp)>>
     | Some f -> <:expr< $lid:f$>> in
   let substitute = match h with
     | None ->
@@ -160,10 +220,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let rawwit = <:expr< $lid:"rawwit_"^s$ >> in
   let globwit = <:expr< $lid:"globwit_"^s$ >> in
   let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
+  let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in
   declare_str_items loc
    [ <:str_item<
       value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) =
-      Genarg.create_arg $se$ >>;
+      Genarg.create_arg $default_value$ $se$>>;
      <:str_item<
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
      <:str_item< do {
@@ -171,7 +232,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
         ((fun e x ->
           (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))),
         (fun ist gl x ->
-          (Genarg.in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))),
+	  let (sigma,a_interp) = $interp$ ist gl (out_gen $globwit$ x) in
+          (sigma , Genarg.in_gen $wit$ a_interp)),
         (fun subst x ->
           (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x)))));
       Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a))
@@ -195,7 +257,7 @@ let declare_vernac_argument loc s pr cl =
    [ <:str_item<
       value (($lid:"wit_"^s$:Genarg.abstract_argument_type unit Genarg.tlevel),
              ($lid:"globwit_"^s$:Genarg.abstract_argument_type unit Genarg.glevel),
-              $lid:"rawwit_"^s$) = Genarg.create_arg $se$ >>;
+              $lid:"rawwit_"^s$) = Genarg.create_arg None $se$ >>;
      <:str_item<
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
     <:str_item< do {
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 4418a45f..82f24242 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -106,11 +106,14 @@ let make_constr_action
   in
   make ([],[],[]) (List.rev pil)
 
+let check_cases_pattern_env loc (env,envlist,hasbinders) =
+  if hasbinders then error_invalid_pattern_notation loc else (env,envlist)
+
 let make_cases_pattern_action
   (f : loc -> cases_pattern_notation_substitution -> cases_pattern_expr) pil =
-  let rec make (env,envlist as fullenv) = function
+  let rec make (env,envlist,hasbinders as fullenv) = function
   | [] ->
-      Gram.action (fun loc -> f loc fullenv)
+      Gram.action (fun loc -> f loc (check_cases_pattern_env loc fullenv))
   | (GramConstrTerminal _ | GramConstrNonTerminal (_,None)) :: tl ->
       (* parse a non-binding item *)
       Gram.action (fun _ -> make fullenv tl)
@@ -118,28 +121,37 @@ let make_cases_pattern_action
       (* parse a binding non-terminal *)
     (match typ with
     | ETConstr _ -> (* pattern non-terminal *)
-        Gram.action (fun (v:cases_pattern_expr) -> make (v::env,envlist) tl)
+        Gram.action (fun (v:cases_pattern_expr) ->
+          make (v::env, envlist, hasbinders) tl)
     | ETReference ->
         Gram.action (fun (v:reference) ->
-	  make (CPatAtom (dummy_loc,Some v) :: env, envlist) tl)
+	  make (CPatAtom (dummy_loc,Some v) :: env, envlist, hasbinders) tl)
     | ETName ->
         Gram.action (fun (na:name located) ->
-	  make (cases_pattern_expr_of_name na :: env, envlist) tl)
+	  make (cases_pattern_expr_of_name na :: env, envlist, hasbinders) tl)
     | ETBigint ->
         Gram.action (fun (v:Bigint.bigint) ->
-	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist) tl)
+	  make (CPatPrim (dummy_loc,Numeral v) :: env, envlist, hasbinders) tl)
     | ETConstrList (_,_) ->
         Gram.action  (fun (vl:cases_pattern_expr list) ->
-	  make (env, vl :: envlist) tl)
-    | (ETPattern | ETBinderList _ | ETBinder _ | ETOther _) ->
-	failwith "Unexpected entry of type cases pattern or other")
+	  make (env, vl :: envlist, hasbinders) tl)
+    | ETBinder _ | ETBinderList (true,_) ->
+	Gram.action (fun (v:local_binder list) ->
+	  make (env, envlist, hasbinders) tl)
+    | ETBinderList (false,_) ->
+	Gram.action (fun (v:local_binder list list) ->
+	  make (env, envlist, true) tl)
+    | (ETPattern | ETOther _) ->
+        anomaly "Unexpected entry of type cases pattern or other")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
       let heads,env = list_chop n env in
-      if b then make (env,(heads@List.hd envlist)::List.tl envlist) tl
-      else make (env,heads::envlist) tl
+      if b then
+        make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl
+      else
+        make (env,heads::envlist,hasbinders) tl
   in
-  make ([],[]) (List.rev pil)
+  make ([],[],false) (List.rev pil)
 
 let rec make_constr_prod_item assoc from forpat = function
   | GramConstrTerminal tok :: l ->
@@ -349,3 +361,8 @@ let _ =
     { freeze_function = freeze;
       unfreeze_function = unfreeze;
       init_function = init }
+
+let with_grammar_rule_protection f x =
+  let fs = freeze () in
+  try let a = f x in unfreeze fs; a
+  with e -> unfreeze fs; raise e
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index 1d85c74e..0ac46ded 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -71,3 +71,5 @@ val get_extend_vernac_grammars :
 val recover_notation_grammar :
   notation -> (precedence * tolerability list) ->
   notation_var_internalization_type list * notation_grammar
+
+val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index ce734622..0398f0b6 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -15,12 +15,12 @@ open Genarg
 
 let tactic_main_level = 5
 
-let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0"
-let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1"
-let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2"
-let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3"
-let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4"
-let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5"
+let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg None "tactic0"
+let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg None "tactic1"
+let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg None "tactic2"
+let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg None "tactic3"
+let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg None "tactic4"
+let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg None "tactic5"
 
 let wit_tactic = function
   | 0 -> wit_tactic0
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 5d5f6e4d..958f59e0 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -31,6 +31,11 @@ let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
 
+let binders_of_names l =
+  List.map (fun (loc, na) ->
+    LocalRawAssum ([loc, na], Default Explicit,
+		   CHole (loc, Some (Evd.BinderType na)))) l
+
 let binders_of_lidents l =
   List.map (fun (loc, id) ->
     LocalRawAssum ([loc, Name id], Default Glob_term.Explicit,
@@ -95,15 +100,21 @@ let impl_ident_head =
 	      | _ -> err ())
 	| _ -> err ())
 
-let ident_colon =
-  Gram.Entry.of_parser "ident_colon"
+let name_colon =
+  Gram.Entry.of_parser "name_colon"
     (fun strm ->
       match get_tok (stream_nth 0 strm) with
 	| IDENT s ->
             (match get_tok (stream_nth 1 strm) with
               | KEYWORD ":" ->
                   stream_njunk 2 strm;
-                  Names.id_of_string s
+                  Name (Names.id_of_string s)
+              | _ -> err ())
+	| KEYWORD "_" ->
+          (match get_tok (stream_nth 1 strm) with
+              | KEYWORD ":" ->
+                  stream_njunk 2 strm;
+                  Anonymous
               | _ -> err ())
         | _ -> err ())
 
@@ -378,8 +389,7 @@ GEXTEND Gram
           [LocalRawAssum (id::idl,Default Explicit,c)]
 	(* binders factorized with open binder *)
       | id = name; idl = LIST0 name; bl = binders ->
-          let t = CHole (loc, Some (Evd.BinderType (snd id))) in
-          LocalRawAssum (id::idl,Default Explicit,t)::bl
+          binders_of_names (id::idl) @ bl
       | id1 = name; ".."; id2 = name ->
           [LocalRawAssum ([id1;(loc,Name ldots_var);id2],
 	                  Default Explicit,CHole (loc,None))]
@@ -421,8 +431,8 @@ GEXTEND Gram
     [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c
       | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
 	  id, expl, c
-      | iid=ident_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
-	  (loc, Name iid), expl, c
+      | iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
+	  (loc, iid), expl, c
       | c = operconstr LEVEL "200" ->
 	  (loc, Anonymous), false, c
     ] ]
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 9abb8cd1..23e7e31b 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -23,11 +23,6 @@ let thm_token = G_vernac.thm_token
 GEXTEND Gram
   GLOBAL: command;
 
-  destruct_location :
-  [ [ IDENT "Conclusion"  -> Tacexpr.ConclLocation ()
-    | discard = [ IDENT "Discardable" -> true | -> false ]; "Hypothesis"
-	-> Tacexpr.HypLocation discard ] ]
-  ;
   opt_hintbases:
   [ [ -> []
     | ":"; l = LIST1 [id = IDENT -> id ] -> l ] ]
@@ -58,9 +53,6 @@ GEXTEND Gram
       | IDENT "Defined" -> VernacEndProof (Proved (false,None))
       |	IDENT "Defined"; id=identref ->
 	  VernacEndProof (Proved (false,Some (id,None)))
-      | IDENT "Suspend" -> VernacSuspend
-      | IDENT "Resume" -> VernacResume None
-      | IDENT "Resume"; id = identref -> VernacResume (Some id)
       | IDENT "Restart" -> VernacRestart
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
@@ -68,9 +60,7 @@ GEXTEND Gram
       | IDENT "Focus" -> VernacFocus None
       | IDENT "Focus"; n = natural -> VernacFocus (Some n)
       | IDENT "Unfocus" -> VernacUnfocus
-      | IDENT "BeginSubproof" -> VernacSubproof None
-      | IDENT "BeginSubproof"; n = natural -> VernacSubproof (Some n)
-      | IDENT "EndSubproof" -> VernacEndSubproof
+      | IDENT "Unfocused" -> VernacUnfocused
       | IDENT "Show" -> VernacShow (ShowGoal OpenSubgoals)
       | IDENT "Show"; n = natural -> VernacShow (ShowGoal (NthGoal n))
       | IDENT "Show"; IDENT "Goal"; n = string ->
@@ -118,14 +108,7 @@ GEXTEND Gram
       | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
       | IDENT "Extern"; n = natural; c = OPT constr_pattern ; "=>";
           tac = tactic ->
-	  HintsExtern (n,c,tac)
-      | IDENT "Destruct";
-          id = ident; ":=";
-          pri = natural;
-          dloc = destruct_location;
-          hyptyp = constr_pattern;
-          "=>"; tac = tactic ->
-            HintsDestruct(id,pri,dloc,hyptyp,tac) ] ]
+	  HintsExtern (n,c,tac) ] ]
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f1b3ffed..34590fb1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -348,7 +348,7 @@ GEXTEND Gram
       | IDENT "lazy"; s = strategy_flag -> Lazy s
       | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
       | IDENT "vm_compute" -> CbvVm
-      | 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 SEP"," -> Pattern pl
       | s = IDENT -> ExtraRedExpr s ] ]
@@ -597,21 +597,18 @@ GEXTEND Gram
 
       (* Automation tactic *)
       | IDENT "trivial"; lems = auto_using; db = hintbases ->
-	  TacTrivial (lems,db)
+          TacTrivial (Off,lems,db)
+      | IDENT "info_trivial"; lems = auto_using; db = hintbases ->
+          TacTrivial (Info,lems,db)
+      | IDENT "debug"; IDENT "trivial"; lems = auto_using; db = hintbases ->
+          TacTrivial (Debug,lems,db)
+
       | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
-	  TacAuto (n,lems,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"; IDENT "decomp"; p = OPT natural;
-          lems = auto_using -> TacDAuto (None,p,lems)
-      | IDENT "auto"; n = OPT int_or_var; IDENT "decomp"; p = OPT natural;
-          lems = auto_using -> TacDAuto (n,p,lems)
+          TacAuto (Off,n,lems,db)
+      | IDENT "info_auto"; n = OPT int_or_var; lems = auto_using;
+          db = hintbases -> TacAuto (Info,n,lems,db)
+      | IDENT "debug"; IDENT "auto"; n = OPT int_or_var; lems = auto_using;
+          db = hintbases -> TacAuto (Debug,n,lems,db)
 
       (* Context management *)
       | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ac81786b..333934be 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -143,7 +143,7 @@ let test_plurial_form_types = function
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    typeclass_constraint record_field decl_notation rec_definition;
+    record_field decl_notation rec_definition;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)
@@ -656,6 +656,7 @@ GEXTEND Gram
       | IDENT "clear"; IDENT "implicits" -> [`ClearImplicits]
       | IDENT "clear"; IDENT "scopes" -> [`ClearScopes]
       | IDENT "rename" -> [`Rename]
+      | IDENT "extra"; IDENT "scopes" -> [`ExtraScopes]
       | IDENT "clear"; IDENT "scopes"; IDENT "and"; IDENT "implicits" ->
           [`ClearImplicits; `ClearScopes]
       | IDENT "clear"; IDENT "implicits"; IDENT "and"; IDENT "scopes" ->
@@ -927,7 +928,6 @@ GEXTEND Gram
 
 (* Resetting *)
       | IDENT "Reset"; id = identref -> VernacResetName id
-      | IDENT "Delete"; id = identref -> VernacRemoveName id
       | IDENT "Reset"; IDENT "Initial" -> VernacResetInitial
       | IDENT "Back" -> VernacBack 1
       | IDENT "Back"; n = natural -> VernacBack n
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 4970ca13..fa075536 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -219,25 +219,33 @@ let surround_impl k p =
   | Explicit -> str"(" ++ p ++ str")"
   | Implicit -> str"{" ++ p ++ str"}"
 
-let surround_binder k p =
-  match k with
-  | Default b -> hov 1 (surround_impl b p)
-  | Generalized (b, b', t) ->
-      hov 1 (surround_impl b' (surround_impl b p))
-
 let surround_implicit k p =
   match k with
-  | Default Explicit -> p
-  | Default Implicit -> (str"{" ++ p ++ str"}")
-  | Generalized (b, b', t) ->
-      surround_impl b' (surround_impl b p)
+  | Explicit -> p
+  | Implicit -> (str"{" ++ p ++ str"}")
 
 let pr_binder many pr (nal,k,t) =
-  match t with
-  | CHole _ -> prlist_with_sep spc pr_lname nal
-  | _ ->
-    let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
-      hov 1 (if many then surround_binder k s else surround_implicit k s)
+  match k with
+    | Generalized (b, b', t') ->
+      assert (b=Implicit);
+      begin match nal with
+	|[loc,Anonymous] ->
+	  hov 1 (str"`" ++ (surround_impl b'
+			      ((if t' then str "!" else mt ()) ++ pr t)))
+	|[loc,Name id] ->
+	  hov 1 (str "`" ++ (surround_impl b'
+			       (pr_lident (loc,id) ++ str " : " ++
+				  (if t' then str "!" else mt()) ++ pr t)))
+	|_ -> anomaly "List of generalized binders have alwais one element."
+      end
+    | Default b ->
+      match t with
+	| CHole _ ->
+	  let s = prlist_with_sep spc pr_lname nal in
+	  hov 1 (surround_implicit b s)
+	| _ ->
+	  let s = prlist_with_sep spc pr_lname nal ++ str " : " ++ pr t in
+	  hov 1 (if many then surround_impl b s else surround_implicit b s)
 
 let pr_binder_among_many pr_c = function
   | LocalRawAssum (nal,k,t) ->
@@ -323,19 +331,27 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
   pr_opt_type_spc pr t ++ str " :=" ++
   pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
-let pr_fixdecl pr prd dangling_with_for ((_,id),(n,ro),bl,t,c) =
-  let annot =
-    match ro with
-	CStructRec ->
-	  if List.length bl > 1 && n <> None then
-	    spc() ++ str "{struct " ++ pr_id (snd (Option.get n)) ++ str"}"
-	  else mt()
-      | CWfRec c ->
-	  spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
-      | CMeasureRec (m,r) ->
-	  spc () ++ str "{measure " ++ pr lsimple m ++ pr_id (snd (Option.get n)) ++
-	    (match r with None -> mt() | Some r -> str" on " ++ pr lsimple r) ++ str"}"
-  in
+let pr_guard_annot pr_aux bl (n,ro) =
+  match n with
+    | None -> mt ()
+    | Some (loc, id) ->
+      match (ro : Topconstr.recursion_order_expr) with
+	| CStructRec ->
+	  let names_of_binder = function
+	    | LocalRawAssum (nal,_,_) -> nal
+	    | LocalRawDef (_,_) -> []
+	  in let ids = List.flatten (List.map names_of_binder bl) in
+	     if List.length ids > 1 then
+	       spc() ++ str "{struct " ++ pr_id id ++ str"}"
+	     else mt()
+	| CWfRec c ->
+	  spc() ++ str "{wf " ++ pr_aux c ++ spc() ++ pr_id id ++ str"}"
+	| CMeasureRec (m,r) ->
+	  spc() ++ str "{measure " ++ pr_aux m ++ spc() ++ pr_id id++
+	    (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
+
+let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) =
+  let annot = pr_guard_annot (pr lsimple) bl ro in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
 let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) =
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index f9ed3af0..afcdad3e 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -51,12 +51,16 @@ val pr_with_occurrences :
   ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
 val pr_red_expr :
   ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
-    ('a,'b,'c) red_expr_gen -> std_ppcmds
+  ('a,'b,'c) red_expr_gen -> std_ppcmds
 val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
   ('c -> std_ppcmds) -> ('a,'b,'c) may_eval -> std_ppcmds
 
 val pr_glob_sort : glob_sort -> std_ppcmds
+val pr_guard_annot : (constr_expr -> std_ppcmds) ->
+  local_binder list ->
+  ('a * Names.identifier) option * recursion_order_expr ->
+  std_ppcmds
 
 val pr_binders : local_binder list -> std_ppcmds
 val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 3305acb7..6e13d4e9 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -515,6 +515,11 @@ let pr_auto_using prc = function
   | l -> spc () ++
       hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
+let string_of_debug = function
+  | Off -> ""
+  | Debug -> "debug "
+  | Info -> "info_"
+
 let pr_then () = str ";"
 
 let ltop = (5,E)
@@ -623,19 +628,14 @@ let rec pr_atom0 = function
   | TacAssumption -> str "assumption"
   | TacAnyConstructor (false,None) -> str "constructor"
   | TacAnyConstructor (true,None) -> str "econstructor"
-  | TacTrivial ([],Some []) -> str "trivial"
-  | TacAuto (None,[],Some []) -> str "auto"
+  | TacTrivial (d,[],Some []) -> str (string_of_debug d ^ "trivial")
+  | TacAuto (d,None,[],Some []) -> str (string_of_debug d ^ "auto")
   | TacReflexivity -> str "reflexivity"
   | TacClear (true,[]) -> str "clear"
   | t -> str "(" ++ pr_atom1 t ++ str ")"
 
   (* Main tactic printer *)
 and pr_atom1 = function
-  | TacAutoTDB _ | TacDestructHyp _ | TacDestructConcl
-  | TacSuperAuto _ | TacExtend (_,
-    ("GTauto"|"GIntuition"|"TSimplif"|
-     "LinearIntuition"),_) ->
-      errorlabstrm "Obsolete V8" (str "Tactic is not ported to V8.0")
   | TacExtend (loc,s,l) ->
       pr_with_comments loc (pr_extend 1 s l)
   | TacAlias (loc,s,l,_) ->
@@ -742,17 +742,15 @@ and pr_atom1 = function
       hov 1 (str "lapply" ++ pr_constrarg c)
 
   (* Automation tactics *)
-  | TacTrivial ([],Some []) as x -> pr_atom0 x
-  | TacTrivial (lems,db) ->
-      hov 0 (str "trivial" ++
+  | TacTrivial (_,[],Some []) as x -> pr_atom0 x
+  | TacTrivial (d,lems,db) ->
+      hov 0 (str (string_of_debug d ^ "trivial") ++
              pr_auto_using pr_constr lems ++ pr_hintbases db)
-  | TacAuto (None,[],Some []) as x -> pr_atom0 x
-  | TacAuto (n,lems,db) ->
-      hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++
+  | TacAuto (_,None,[],Some []) as x -> pr_atom0 x
+  | TacAuto (d,n,lems,db) ->
+      hov 0 (str (string_of_debug d ^ "auto") ++
+	     pr_opt (pr_or_var int) n ++
              pr_auto_using pr_constr lems ++ pr_hintbases db)
-  | TacDAuto (n,p,lems) ->
-      hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++
-             pr_opt int p ++ pr_auto_using pr_constr lems)
 
   (* Context management *)
   | TacClear (true,[]) as t -> pr_atom0 t
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index c858439e..cf9d4a53 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -203,11 +203,7 @@ let pr_hints local db h pr_c pr_pat =
 	let pat = match c with None -> mt () | Some pat -> pr_pat pat in
           str "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
           spc() ++ pr_raw_tactic tac
-    | HintsDestruct(name,i,loc,c,tac) ->
-        str "Destruct " ++ pr_id name ++ str" :=" ++ spc() ++
-        hov 0 (int i ++ spc() ++ pr_destruct_location loc ++ spc() ++
-               pr_c c ++ str " =>") ++ spc() ++
-        pr_raw_tactic tac in
+  in
   hov 2 (str"Hint "++pr_locality local ++ pph ++ opth)
 
 let pr_with_declaration pr_c = function
@@ -292,28 +288,6 @@ let pr_binders_arg =
 let pr_and_type_binders_arg bl =
   pr_binders_arg bl
 
-let names_of_binder = function
-  | LocalRawAssum (nal,_,_) -> nal
-  | LocalRawDef (_,_) -> []
-
-let pr_guard_annot bl (n,ro) =
-  match n with
-  | None -> mt ()
-  | Some (loc, id) ->
-      match (ro : Topconstr.recursion_order_expr) with
-      | CStructRec ->
-          let ids = List.flatten (List.map names_of_binder bl) in
-	  if List.length ids > 1 then
-	    spc() ++ str "{struct " ++ pr_id id ++ str"}"
-	  else mt()
-      | CWfRec c ->
-	  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++
-	  pr_id id ++ str"}"
-      | CMeasureRec (m,r) ->
-	  spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++
-	  pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++
-	    pr_lconstr_expr r) ++ str"}"
-
 let pr_onescheme (idop,schem) =
   match schem with
   | InductionScheme (dep,ind,s) ->
@@ -419,7 +393,7 @@ let pr_statement head (id,(bl,c,guard)) =
   hov 1
     (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
     (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
-    pr_opt (pr_guard_annot bl) guard ++
+    pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
     str":" ++ pr_spc_lconstr c)
 
 (**************************************)
@@ -462,11 +436,10 @@ let rec pr_vernac = function
   (* Proof management *)
   | VernacAbortAll -> str "Abort All"
   | VernacRestart -> str"Restart"
-  | VernacSuspend -> str"Suspend"
   | VernacUnfocus -> str"Unfocus"
+  | VernacUnfocused -> str"Unfocused"
   | VernacGoal c -> str"Goal" ++ pr_lconstrarg c
   | VernacAbort id -> str"Abort" ++ pr_opt pr_lident id
-  | VernacResume id -> str"Resume" ++ pr_opt pr_lident id
   | VernacUndo i -> if i=1 then str"Undo" else str"Undo" ++ pr_intarg i
   | VernacUndoTo i -> str"Undo" ++ spc() ++ str"To" ++ pr_intarg i
   | VernacBacktrack (i,j,k) ->
@@ -493,7 +466,6 @@ let rec pr_vernac = function
   | VernacCheckGuard -> str"Guarded"
 
   (* Resetting *)
-  | VernacRemoveName id -> str"Remove" ++ spc() ++ pr_lident id
   | VernacResetName id -> str"Reset" ++ spc() ++ pr_lident id
   | VernacResetInitial -> str"Reset Initial"
   | VernacBack i -> if i=1 then str"Back" else str"Back" ++ pr_intarg i
@@ -627,7 +599,7 @@ let rec pr_vernac = function
         let (_,_,_,k,_),_ = List.hd l in
 	match k with Record -> "Record" | Structure -> "Structure"
 	  | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
-	  | Class b -> if b then "Definitional Class" else "Class" in
+	  | Class _ -> "Class" in
       hov 1 (pr_oneind key (List.hd l)) ++
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
 
@@ -635,10 +607,10 @@ let rec pr_vernac = function
   | VernacFixpoint recs ->
       let pr_onerec = function
         | ((loc,id),ro,bl,type_,def),ntn ->
-            let annot = pr_guard_annot bl ro in
-            pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
+            let annot = pr_guard_annot pr_lconstr_expr bl ro in
+            pr_id id ++ pr_binders_arg bl ++ annot
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
-            ++ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
+            ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	    prlist (pr_decl_notation pr_constr) ntn
       in
       hov 0 (str "Fixpoint" ++ spc() ++
@@ -690,34 +662,23 @@ let rec pr_vernac = function
 	spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++
 	spc() ++ pr_class_rawexpr c2)
 
-
-(*   | VernacClass (id, par, ar, sup, props) -> *)
-(*       hov 1 ( *)
-(* 	str"Class" ++ spc () ++ pr_lident id ++ *)
-(* (\* 	  prlist_with_sep (spc) (pr_lident_constr (spc() ++ str ":" ++ spc())) par ++  *\) *)
-(* 	  pr_and_type_binders_arg par ++ *)
-(* 	  (match ar with Some ar -> spc () ++ str":" ++ spc() ++ pr_glob_sort (snd ar) | None -> mt()) ++ *)
-(* 	  spc () ++ str":=" ++ spc () ++ *)
-(* 	  prlist_with_sep (fun () -> str";" ++ spc())  *)
-(* 	  (fun (lid,oc,c) -> pr_lident_constr ((if oc then str" :>" else str" :") ++ spc()) (lid,c)) props ) *)
-
  | VernacInstance (abst,glob, sup, (instid, bk, cl), props, pri) ->
      hov 1 (
        pr_non_locality (not glob) ++
        (if abst then str"Declare " else mt ()) ++
-       str"Instance" ++ spc () ++
-	 pr_and_type_binders_arg sup ++
-	 str"=>" ++ spc () ++
-	 (match snd instid with Name id -> pr_lident (fst instid, id) ++ spc () ++ str":" ++ spc () | Anonymous -> mt ()) ++
-	 pr_constr_expr cl ++ spc () ++
+       str"Instance" ++ 
+       (match snd instid with Name id -> spc () ++ pr_lident (fst instid, id) ++ spc () | 
+	Anonymous -> mt ()) ++
+       pr_and_type_binders_arg sup ++
+       str":" ++ spc () ++	 
+       pr_constr_expr cl ++ spc () ++
 	 (match props with
 	  | Some p -> spc () ++ str":=" ++ spc () ++ pr_constr_expr p
 	  | None -> mt()))
 
  | VernacContext l ->
      hov 1 (
-       str"Context" ++ spc () ++ str"[" ++ spc () ++
-	 pr_and_type_binders_arg l ++ spc () ++ str "]")
+       str"Context" ++ spc () ++ pr_and_type_binders_arg l)
 
 
  | VernacDeclareInstances (glob, ids) ->
@@ -817,8 +778,8 @@ let rec pr_vernac = function
       pr_hints local dbnames h pr_constr pr_constr_pattern_expr
   | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
       hov 2
-        (pr_locality local ++ str"Notation " ++ pr_lident id ++
-	 prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++
+        (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++
+	 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
   | VernacDeclareImplicits (local,q,[]) ->
       hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++ 
@@ -852,6 +813,7 @@ let rec pr_vernac = function
         | `SimplNeverUnfold -> str "simpl never"
         | `DefaultImplicits -> str "default implicits"
         | `Rename -> str "rename"
+        | `ExtraScopes -> str "extra scopes"
         | `ClearImplicits -> str "clear implicits"
         | `ClearScopes -> str "clear scopes")
         mods)
@@ -978,9 +940,9 @@ let rec pr_vernac = function
       | Star -> str"*"
       | Plus -> str"+"
   end ++ spc()
-  | VernacSubproof None -> str "BeginSubproof"
+  | VernacSubproof None -> str "{"
   | VernacSubproof (Some i) -> str "BeginSubproof " ++ pr_int i
-  | VernacEndSubproof -> str "EndSubproof"
+  | VernacEndSubproof -> str "}"
 
 and pr_extend s cl =
   let pr_arg a =
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 0b9ce918..5352e0b7 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -35,13 +35,19 @@ let delayed_emacs_cmd s =
 (**********************************************************************)
 (** Terms                                                             *)
 
-  (* [at_top] means ids of env must be avoided in bound variables *)
-let pr_constr_core at_top env t =
-  pr_constr_expr (extern_constr at_top env t)
-let pr_lconstr_core at_top env t =
-  pr_lconstr_expr (extern_constr at_top env t)
+(* [goal_concl_style] means that all names of goal/section variables
+   and all names of rel variables (if any) in the given env and all short
+   names of global definitions of the current module must be avoided while
+   printing bound variables.
+   Otherwise, short names of global definitions are printed qualified
+   and only names of goal/section variables and rel names that do
+   _not_ occur in the scope of the binder to be printed are avoided. *)
+
+let pr_constr_core goal_concl_style env t =
+  pr_constr_expr (extern_constr goal_concl_style env t)
+let pr_lconstr_core goal_concl_style env t =
+  pr_lconstr_expr (extern_constr goal_concl_style env t)
 
-let pr_lconstr_env_at_top env = pr_lconstr_core true env
 let pr_lconstr_env env = pr_lconstr_core false env
 let pr_constr_env env = pr_constr_core false env
 
@@ -68,12 +74,12 @@ let pr_lconstr_under_binders_env = pr_constr_under_binders_env_gen pr_lconstr_en
 let pr_constr_under_binders c = pr_constr_under_binders_env (Global.env()) c
 let pr_lconstr_under_binders c = pr_lconstr_under_binders_env (Global.env()) c
 
-let pr_type_core at_top env t =
-  pr_constr_expr (extern_type at_top env t)
-let pr_ltype_core at_top env t =
-  pr_lconstr_expr (extern_type at_top env t)
+let pr_type_core goal_concl_style env t =
+  pr_constr_expr (extern_type goal_concl_style env t)
+let pr_ltype_core goal_concl_style env t =
+  pr_lconstr_expr (extern_type goal_concl_style env t)
 
-let pr_ltype_env_at_top env = pr_ltype_core true env
+let pr_goal_concl_style_env env = pr_ltype_core true env
 let pr_ltype_env env = pr_ltype_core false env
 let pr_type_env env = pr_type_core false env
 
@@ -262,7 +268,7 @@ let default_pr_goal gs =
   let preamb,thesis,penv,pc =
     mt (), mt (),
     pr_context_of env,
-    pr_ltype_env_at_top env (Goal.V82.concl sigma g)
+    pr_goal_concl_style_env env (Goal.V82.concl sigma g)
   in
     preamb ++
     str"  " ++ hv 0 (penv ++ fnl () ++
@@ -279,7 +285,7 @@ let pr_goal_tag g =
 let pr_concl n sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
   let env = Goal.V82.env sigma g in
-  let pc = pr_ltype_env_at_top env (Goal.V82.concl sigma g) in
+  let pc = pr_goal_concl_style_env env (Goal.V82.concl sigma g) in
     str (emacs_str "")  ++
       str "subgoal " ++ int n ++ pr_goal_tag g ++
       str " is:" ++ cut () ++ str" "  ++ pc
@@ -363,7 +369,8 @@ let default_pr_subgoals close_cmd sigma seeds = function
 		let pei = pr_evars_int 1 exl in
 		  (str "No more subgoals but non-instantiated existential " ++
 		     str "variables:" ++ fnl () ++ (hov 0 pei)
-		   ++ emacs_print_dependent_evars sigma seeds)
+		   ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
+                   str "You can use Grab Existential Variables.")
       end
   | [g] ->
       let pg = default_pr_goal { it = g ; sigma = sigma } in
@@ -424,7 +431,7 @@ let pr_open_subgoals () =
             begin match bgoals with
 	    | [] -> pr_subgoals None sigma seeds goals
 	    | _ -> pr_subgoals None bsigma seeds bgoals ++ fnl () ++ fnl () ++
-		      str"This subproof is complete, but there are still unfocused goals:"
+		      str"This subproof is complete, but there are still unfocused goals." ++ fnl ()
 		(* spiwack: to stay compatible with the proof general and coqide,
 		    I use print the message after the goal. It would be better to have
 		    something like:
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 2d437c20..bbc3a6ca 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -26,7 +26,6 @@ open Tacexpr
 (** Terms *)
 
 val pr_lconstr_env         : env -> constr -> std_ppcmds
-val pr_lconstr_env_at_top  : env -> constr -> std_ppcmds
 val pr_lconstr             : constr -> std_ppcmds
 
 val pr_constr_env          : env -> constr -> std_ppcmds
@@ -44,7 +43,7 @@ val pr_constr_under_binders      : constr_under_binders -> std_ppcmds
 val pr_lconstr_under_binders_env : env -> constr_under_binders -> std_ppcmds
 val pr_lconstr_under_binders     : constr_under_binders -> std_ppcmds
 
-val pr_ltype_env_at_top    : env -> types -> std_ppcmds
+val pr_goal_concl_style_env : env -> types -> std_ppcmds
 val pr_ltype_env           : env -> types -> std_ppcmds
 val pr_ltype               : types -> std_ppcmds
 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 7df97a07..6e3b3f35 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -273,6 +273,11 @@ let mlexpr_of_message_token = function
   | Tacexpr.MsgInt n -> <:expr< Tacexpr.MsgInt $mlexpr_of_int n$ >>
   | Tacexpr.MsgIdent id -> <:expr< Tacexpr.MsgIdent $mlexpr_of_hyp id$ >>
 
+let mlexpr_of_debug = function
+  | Tacexpr.Off -> <:expr< Tacexpr.Off >>
+  | Tacexpr.Debug -> <:expr< Tacexpr.Debug >>
+  | Tacexpr.Info -> <:expr< Tacexpr.Info >>
+
 let rec mlexpr_of_atomic_tactic = function
   (* Basic tactics *)
   | Tacexpr.TacIntroPattern pl ->
@@ -399,15 +404,17 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >>
 
   (* Automation tactics *)
-  | Tacexpr.TacAuto (n,lems,l) ->
+  | Tacexpr.TacAuto (debug,n,lems,l) ->
+      let d = mlexpr_of_debug debug in
       let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
       let lems = mlexpr_of_list mlexpr_of_constr lems in
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
-      <:expr< Tacexpr.TacAuto $n$ $lems$ $l$ >>
-  | Tacexpr.TacTrivial (lems,l) ->
+      <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >>
+  | Tacexpr.TacTrivial (debug,lems,l) ->
+      let d = mlexpr_of_debug debug in
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
       let lems = mlexpr_of_list mlexpr_of_constr lems in
-      <:expr< Tacexpr.TacTrivial $lems$ $l$ >>
+      <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >>
 
   | _ -> failwith "Quotation of atomic tactic expressions: TODO"
 
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 2fe1fdda..05fdba42 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -119,20 +119,42 @@ let make_one_printing_rule se (pt,e) =
 
 let make_printing_rule se = mlexpr_of_list (make_one_printing_rule se)
 
-let rec contains_epsilon = function
-  | List0ArgType _ -> true
-  | List1ArgType t -> contains_epsilon t
-  | OptArgType _ -> true
-  | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2
-  | ExtraArgType("hintbases") -> true
-  | _ -> false
-let is_atomic = function
-  | GramTerminal s :: l when
-      List.for_all (function
-          GramTerminal _ -> false
-	| GramNonTerminal(_,t,_,_) -> contains_epsilon t) l
-	-> [s]
-  | _ -> []
+let rec possibly_empty_subentries loc = function
+  | [] -> []
+  | (s,prodsl) :: l ->
+    let rec aux = function
+    | [] -> (false,<:expr< None >>)
+    | prods :: rest ->
+      try
+        let l = List.map (function
+        | GramNonTerminal(_,(List0ArgType _|
+                             OptArgType _|
+                             ExtraArgType _ as t),_,_)->
+            (* This possibly parses epsilon *)
+            let rawwit = make_rawwit loc t in
+            <:expr< match Genarg.default_empty_value $rawwit$ with
+                    [ None -> failwith ""
+                    | Some v ->
+                        Tacinterp.intern_genarg Tacinterp.fully_empty_glob_sign
+                          (Genarg.in_gen $rawwit$ v) ] >>
+        | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
+            (* This does not parse epsilon (this Exit is static time) *)
+             raise Exit) prods in
+        if has_extraarg prods then
+          (true,<:expr< try Some $mlexpr_of_list (fun x -> x) l$
+                        with [ Failure "" -> $snd (aux rest)$ ] >>)
+        else
+          (true, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>)
+      with Exit -> aux rest in
+    let (nonempty,v) = aux prodsl in
+    if nonempty then (s,v) :: possibly_empty_subentries loc l
+    else possibly_empty_subentries loc l
+
+let possibly_atomic loc prods =
+  let l = list_map_filter (function
+    | GramTerminal s :: l, _ -> Some (s,l)
+    | _ -> None) prods in
+  possibly_empty_subentries loc (list_factorize_left l)
 
 let declare_tactic loc s cl =
   let se = mlexpr_of_string s in
@@ -151,17 +173,20 @@ let declare_tactic loc s cl =
   in
   let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in
   let atomic_tactics =
-    mlexpr_of_list mlexpr_of_string
-      (List.flatten (List.map (fun (al,_) -> is_atomic al) cl)) in
+    mlexpr_of_list (mlexpr_of_pair mlexpr_of_string (fun x -> x))
+      (possibly_atomic loc cl) in
   declare_str_items loc
    (hidden @
     [ <:str_item< do {
       try
         let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in
         List.iter
-          (fun s -> Tacinterp.add_primitive_tactic s
+          (fun (s,l) -> match l with
+           [ Some l ->
+              Tacinterp.add_primitive_tactic s
               (Tacexpr.TacAtom($default_loc$,
-                 Tacexpr.TacExtend($default_loc$,s,[]))))
+                 Tacexpr.TacExtend($default_loc$,$se$,l)))
+           | None -> () ])
           $atomic_tactics$
       with e -> Pp.pp (Errors.print e);
       Egrammar.extend_tactic_grammar $se$ $gl$;