Fixing bug #2732 (anomaly when using the tolerance for writing

"f atomic_tac" as a short-hand for "f ltac:(atomic_tac)" for "f" an
Ltac function - see Tacinterp.add_primitive_tactic).

More precisely, when parsing "f ref" and "ref" is recognized as the
name of some TACTIC-EXTEND-defined tactic parsable as an atomic tactic
(like "eauto", "firstorder", "discriminate", ...), the code was
correct only when a rule of the form `TACTIC EXTEND ... [ "foo" -> ...] END'
was given (where "foo" has no arguments in the rule) but not when a rule
of the form `TACTIC EXTEND ... [ "foo" tactic_opt(p) -> ...] END' was given
(where "foo" had an optional argument in the rule). In particular,
"firstorder" was in this case.

More generally, if, for an extra argument able to parse the empty string, a rule
`TACTIC EXTEND ... [ "foo" my_special_extra_arg(p) -> ...] END' was given,
then "foo" was not recognized as parseable as an atomic string (this
happened e.g. for "eauto").  This is now also fixed.

There was also another bug when the internal name of tactic was not
the same as the user-level name of the tactic. This is the reason why
"congruence" was not recognized when given as argument of an ltac (its
internal name is "cc").

Incidentally removed the redundant last line in the parsing rule for
"firstorder".

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

13 files changed, 168 insertions, 51 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index b4f87d96b3..0d640640b3 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -64,23 +64,10 @@ type 'a with_ebindings = 'a * open_constr bindings
 
 type 'a generic_argument = argument_type * Obj.t
 
-let dyntab = ref ([] : string list)
-
 type rlevel
 type glevel
 type tlevel
 
-type ('a,'b) abstract_argument_type = argument_type
-
-let create_arg s =
-  if List.mem s !dyntab then
-    anomaly ("Genarg.create: already declared generic argument " ^ s);
-  dyntab := s :: !dyntab;
-  let t = ExtraArgType s in
-  (t,t,t)
-
-let exists_argtype s = List.mem s !dyntab
-
 type intro_pattern_expr =
   | IntroOrAndPattern of or_and_intro_pattern_expr
   | IntroWildcard
@@ -260,3 +247,32 @@ let unquote x = x
 type an_arg_of_this_type = Obj.t
 
 let in_generic t x = (t, Obj.repr x)
+
+let dyntab = ref ([] : (string * glevel generic_argument option) list)
+
+type ('a,'b) abstract_argument_type = argument_type
+
+let create_arg v s =
+  if List.mem_assoc s !dyntab then
+    anomaly ("Genarg.create: already declared generic argument " ^ s);
+  let t = ExtraArgType s in
+  dyntab := (s,Option.map (in_gen t) v) :: !dyntab;
+  (t,t,t)
+
+let exists_argtype s = List.mem_assoc s !dyntab
+
+let default_empty_argtype_value s = List.assoc s !dyntab
+
+let default_empty_value t =
+  let rec aux = function
+  | List0ArgType _ -> Some (in_gen t [])
+  | OptArgType _ -> Some (in_gen t None)
+  | PairArgType(t1,t2) ->
+      (match aux t1, aux t2 with
+      | Some (_,v1), Some (_,v2) -> Some (in_gen t (v1,v2))
+      | _ -> None)
+  | ExtraArgType s -> default_empty_argtype_value s
+  | _ -> None in
+  match aux t with
+  | Some v -> Some (out_gen t v)
+  | None -> None
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 9c47c691a9..43cd73aedb 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -257,7 +257,8 @@ val app_pair :
 
 (** create a new generic type of argument: force to associate
    unique ML types at each of the three levels *)
-val create_arg : string ->
+val create_arg : 'globa option ->
+    string ->
       ('a,tlevel) abstract_argument_type
       * ('globa,glevel) abstract_argument_type
       * ('rawa,rlevel) abstract_argument_type
@@ -299,7 +300,6 @@ val in_gen :
 val out_gen :
   ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a
 
-
 (** [in_generic] is used in combination with camlp4 [Gramext.action] magic
 
    [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
@@ -313,3 +313,5 @@ type an_arg_of_this_type
 
 val in_generic :
   argument_type -> an_arg_of_this_type -> 'co generic_argument
+
+val default_empty_value : ('a,glevel) abstract_argument_type -> 'a option
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 788e664e29..d890be142b 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -107,6 +107,72 @@ let rec make_wit loc = function
         value wit = $lid:"wit_"^s$;
       end in WIT.wit >>
 
+let possibly_empty_subentries prods =
+  try
+    Some (List.fold_right (fun e l -> match e with
+    | GramNonTerminal(_,(List0ArgType _| OptArgType _),_,_) ->
+        (* This parses epsilon *) l
+    | GramNonTerminal(_,ExtraArgType s,_,_) ->
+        (* This parses epsilon if s parses it *) s::l
+    | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
+        (* This does not parse epsilon *)
+        (* Not meaningful to have Pair in prods nor to have empty *)
+        (* entries in Lst1 productions *)
+        raise Exit) prods [])
+  with Exit -> None
+
+let has_extraarg =
+  List.exists (function GramNonTerminal(_,ExtraArgType _,_,_) -> true | _ -> false)
+
+let statically_known_possibly_empty (prods,_) =
+  List.for_all (function
+    | GramNonTerminal(_,(OptArgType _|List0ArgType _|ExtraArgType _),_,_) ->
+        (* Opt and List0 parses the empty string and for ExtraArg we don't know *)
+        (* (we'll have to test dynamically *)
+        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< $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_globwit 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 *)
+    (true, <:expr< try Some $aux prods$ with Exit -> None >>)
+  else
+    (* Static optimisation *)
+    (false, aux prods)
+
+let make_possibly_empty_subentries loc cl =
+  let cl = List.filter statically_known_possibly_empty 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)) >>
@@ -160,10 +226,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 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 {
@@ -195,7 +262,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/extrawit.ml b/parsing/extrawit.ml
index cc5b58ee70..a660f910e0 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -16,12 +16,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/tacextend.ml4 b/parsing/tacextend.ml4
index 838c771c6b..b7364efc13 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -120,19 +120,27 @@ 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 possibly_empty_subentries loc s prods =
+  try
+    let l = List.map (function
+    | GramNonTerminal(_,(List0ArgType _|OptArgType _|ExtraArgType _ as t),_,_)->
+        (* This possibly parses epsilon *)
+        let globwit = make_globwit loc t in
+        <:expr< match Genarg.default_empty_value $globwit$ with
+                [ None -> failwith ""
+                | Some v -> Genarg.in_gen $globwit$ v ] >>
+    | GramTerminal _ | GramNonTerminal(_,_,_,_) ->
+        (* This does not parse epsilon (this Exit is static time) *)
+        raise Exit) prods in
+    if has_extraarg prods then
+      [s, <:expr< try Some $mlexpr_of_list (fun x -> x) l$
+                  with Failure "" -> None >>]
+    else
+      [s, <:expr< Some $mlexpr_of_list (fun x -> x) l$ >>]
+  with Exit -> []
+
+let possibly_atomic loc = function
+  | GramTerminal s :: l -> possibly_empty_subentries loc s l
   | _ -> []
 
 let declare_tactic loc s cl =
@@ -152,17 +160,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))
+      (List.flatten (List.map (fun (al,_) -> possibly_atomic loc al) 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$;
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 88e62e46df..b5a2ac82eb 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -103,7 +103,7 @@ let proof_instr = Gram.entry_create "proofmode:instr"
 
 (* [Genarg.create_arg] creates a new embedding into Genarg. *)
 let (wit_proof_instr,globwit_proof_instr,rawwit_proof_instr) =
-  Genarg.create_arg "proof_instr"
+  Genarg.create_arg None "proof_instr"
 let _ = Tacinterp.add_interp_genarg "proof_instr"
   begin
   begin fun e x -> (* declares the globalisation function *)
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index f5b16e43fe..48bb87214a 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -134,8 +134,6 @@ TACTIC EXTEND firstorder
 |   [ "firstorder" tactic_opt(t) firstorder_using(l)
        "with" ne_preident_list(l') ] ->
       [ gen_ground_tac true (Option.map eval_tactic t) l l' ]
-|   [ "firstorder" tactic_opt(t) ] ->
-      [ gen_ground_tac true (Option.map eval_tactic t) [] [] ]
 END
 
 TACTIC EXTEND gintuition
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index f330f9ff92..e8fec0dd84 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -154,7 +154,7 @@ type 'a function_rec_definition_loc_argtype = ((Vernacexpr.fixpoint_expr * Verna
 let (wit_function_rec_definition_loc : Genarg.tlevel function_rec_definition_loc_argtype),
   (globwit_function_rec_definition_loc : Genarg.glevel function_rec_definition_loc_argtype),
   (rawwit_function_rec_definition_loc : Genarg.rlevel function_rec_definition_loc_argtype) =
-  Genarg.create_arg "function_rec_definition_loc"
+  Genarg.create_arg None "function_rec_definition_loc"
 VERNAC COMMAND EXTEND Function
    ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")] ->
 	[
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 0496d758b0..72e18ab140 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -287,13 +287,13 @@ let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x)
 (* spiwack argument for the commands of the retroknowledge *)
 
 let (wit_r_nat_field, globwit_r_nat_field, rawwit_r_nat_field) =
-  Genarg.create_arg "r_nat_field"
+  Genarg.create_arg None "r_nat_field"
 let (wit_r_n_field, globwit_r_n_field, rawwit_r_n_field) =
-  Genarg.create_arg "r_n_field"
+  Genarg.create_arg None "r_n_field"
 let (wit_r_int31_field, globwit_r_int31_field, rawwit_r_int31_field) =
-  Genarg.create_arg "r_int31_field"
+  Genarg.create_arg None "r_int31_field"
 let (wit_r_field, globwit_r_field, rawwit_r_field) =
-  Genarg.create_arg "r_field"
+  Genarg.create_arg None "r_field"
 
 (* spiwack: the print functions are incomplete, but I don't know what they are
 	used for *)
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index a682af04f8..35344c99c2 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -15,6 +15,7 @@ open Termops
 open Glob_term
 
 val rawwit_orient : bool raw_abstract_argument_type
+val globwit_orient : bool glob_abstract_argument_type
 val wit_orient : bool typed_abstract_argument_type
 val orient : bool Pcoq.Gram.entry
 val pr_orient : bool -> Pp.std_ppcmds
@@ -39,6 +40,7 @@ val hloc : loc_place Pcoq.Gram.entry
 val pr_hloc : loc_place -> Pp.std_ppcmds
 
 val in_arg_hyp:  (Names.identifier Pp.located list option * bool)  Pcoq.Gram.entry
+val globwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) glob_abstract_argument_type
 val rawwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) raw_abstract_argument_type
 val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type
 val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Tacticals.clause
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index b8bd166b9b..ba95038187 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1366,7 +1366,7 @@ ARGUMENT EXTEND glob_constr_with_bindings
 END
 
 let _ =
-  (Genarg.create_arg "strategy" :
+  (Genarg.create_arg None "strategy" :
       ((strategy, Genarg.tlevel) Genarg.abstract_argument_type *
 	  (strategy, Genarg.glevel) Genarg.abstract_argument_type *
 	  (strategy, Genarg.rlevel) Genarg.abstract_argument_type))
@@ -1426,6 +1426,8 @@ let clsubstitute o c =
 	  | Some id when is_tac id -> tclIDTAC
 	  | _ -> cl_rewrite_clause c o all_occurrences cl)
 
+open Extraargs
+
 TACTIC EXTEND substitute
 | [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
 END
@@ -1537,7 +1539,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
 
 let _, _, rawwit_binders =
- (Genarg.create_arg "binders" :
+ (Genarg.create_arg None "binders" :
     Genarg.tlevel binders_argtype *
     Genarg.glevel binders_argtype *
     Genarg.rlevel binders_argtype)
diff --git a/test-suite/bugs/closed/shouldsucceed/2732.v b/test-suite/bugs/closed/shouldsucceed/2732.v
new file mode 100644
index 0000000000..f22a8cccc5
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2732.v
@@ -0,0 +1,19 @@
+(* Check correct behavior of add_primitive_tactic in TACEXTEND *)
+
+(* Added also the case of eauto and congruence *)
+
+Ltac thus H := solve [H].
+
+Lemma test: forall n : nat, n <= n.
+Proof.
+  intro.
+  thus firstorder.
+  Undo.
+  thus eauto.
+Qed.
+
+Lemma test2: false = true -> False.
+Proof.
+  intro.
+  thus congruence.
+Qed.
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index 7d155ab41a..9840814b1f 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -61,7 +61,7 @@ type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_a
 let (wit_withtac : Genarg.tlevel withtac_argtype),
   (globwit_withtac : Genarg.glevel withtac_argtype),
   (rawwit_withtac : Genarg.rlevel withtac_argtype) =
-  Genarg.create_arg "withtac"
+  Genarg.create_arg None "withtac"
 
 open Obligations