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

2 files changed, 33 insertions, 15 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