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

3 files changed, 10 insertions, 6 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 0496d758b..72e18ab14 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 a682af04f..35344c99c 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 b8bd166b9..ba9503818 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)