- Inductive types in the "using" option of auto/eauto/firstorder are

  interpreted as using the collection of their constructors as hints.
- Add support for both "using" and "with" in "firstorder". Made the
  syntax of "using" compatible with the one of "auto" by separating
  lemmas by commas. Did not fully merge the syntax: auto accepts
  constr while firstorder accepts names (but are constr really useful?).
- Added "Reserved Infix" as a specific shortcut of the corresponding
  "Reserved Notation".



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

9 files changed, 104 insertions, 37 deletions

diff --git a/CHANGES b/CHANGES
index b02988c8a..3a471e947 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,6 +32,10 @@ Tactics
 - Tactic "exists" and "eexists" supports iteration using
   comma-separated arguments.
 - Tactic "gappa" has been removed from the Dp plugin.
+- Tactic "firstorder" now supports the combination of its "using" and
+  "with" options.
+- An inductive type as argument of the "using" option of "auto/eauto/firstorder"
+  is interpreted as using the collection of its constructors.
 
 Tactic Language
 
@@ -45,6 +49,8 @@ Vernacular commands
 - New support for local binders in the syntax of Record/Structure fields.
 - Most commands referring to constant (e.g. Print or About) now support
   referring to the constant by a notation string.
+- Added "Reserved Infix" as a specific shortcut of the corresponding
+  "Reserved Notation".
 
 Tools
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index abc294e8b..6dbdaedd4 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3115,10 +3115,16 @@ hints of the database named {\tt core}.
   Uses all existing hint databases, minus the special database
   {\tt v62}. See Section~\ref{Hints-databases}
 
-\item \texttt{auto using $lemma_1, \ldots, lemma_n$}
+\item \texttt{auto using \nterm{lemma}$_1$ , \ldots , \nterm{lemma}$_n$}
 
-  Uses $lemma_1, \ldots, lemma_n$ in addition to hints (can be combined
-  with the \texttt{with \ident} option).
+  Uses \nterm{lemma}$_1$, \ldots, \nterm{lemma}$_n$ in addition to
+  hints (can be combined with the \texttt{with \ident} option). If
+  $lemma_i$ is an inductive type, it is the collection of its
+  constructors which is added as hints.
+
+\item \texttt{auto using \nterm{lemma}$_1$ , \ldots , \nterm{lemma}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+
+  This combines the effects of the {\tt using} and {\tt with} options.
 
 \item {\tt trivial}\tacindex{trivial}
 
@@ -3300,11 +3306,17 @@ instead may reason about any first-order class inductive definition.
    Adds lemmas \ident$_1$ \dots\ \ident$_n$ to the proof-search
    environment.
 
- \item {\tt firstorder using \ident$_1$ \dots\ \ident$_n$ }
+ \item {\tt firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ }
    \tacindex{firstorder using}
 
-   Adds lemmas in {\tt auto} hints bases \ident$_1$ \dots\ \ident$_n$
-   to the proof-search environment.
+   Adds lemmas in {\tt auto} hints bases {\qualid}$_1$ \dots\ {\qualid}$_n$
+   to the proof-search environment. If {\qualid}$_i$ refers to an inductive
+   type, it is the collection of its constructors which is added as hints.
+
+\item \texttt{firstorder using {\qualid}$_1$ , \dots\ , {\qualid}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+
+  This combines the effects of the {\tt using} and {\tt with} options.
+
 \end{Variants}
 
 Proof-search is bounded by a depth parameter which can be set by typing the
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 272737cc6..2a5dc64bc 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -833,6 +833,10 @@ GEXTEND Gram
 	 pil = LIST1 production_item; ":="; t = Tactic.tactic
          -> VernacTacticNotation (n,pil,t)
 
+     | IDENT "Reserved"; IDENT "Infix"; s = ne_string;
+	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
+	   VernacSyntaxExtension (use_locality (),("_ '"^s^"' _",l))
+
      | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; 
 	 s = ne_string; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 96c5bcae4..8302da5c1 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -58,12 +58,7 @@ let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
 
 let fail_solver=tclFAIL 0 (Pp.str "GTauto failed")
 		      
-type external_env=
-    Ids of global_reference list
-  | Bases of Auto.hint_db_name list
-  | Void
-
-let gen_ground_tac flag taco ext gl=
+let gen_ground_tac flag taco ids bases gl=
   let backup= !qflag in
     try
       qflag:=flag;
@@ -71,11 +66,9 @@ let gen_ground_tac flag taco ext gl=
 	match taco with 
 	    Some tac-> tac
 	  | None-> default_solver in
-      let startseq=
-	match ext with
-	    Void -> (fun gl -> empty_seq !ground_depth)
-	  | Ids l-> create_with_ref_list l !ground_depth
-	  | Bases l-> create_with_auto_hints l !ground_depth in
+      let startseq gl=
+	let seq=empty_seq !ground_depth in
+	extend_with_auto_hints bases (extend_with_ref_list ids seq gl) gl in
       let result=ground_tac solver startseq gl in 
 	qflag:=backup;result
     with e ->qflag:=backup;raise e
@@ -96,18 +89,45 @@ let normalize_evaluables=
 	   unfold_in_hyp (Lazy.force defined_connectives) 
 	   (Tacexpr.InHypType id)) *)
 
+open Genarg
+open Ppconstr
+open Printer
+let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_coma pr_reference
+let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_coma (pr_or_var (pr_located pr_global))
+let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_coma pr_global
+
+ARGUMENT EXTEND firstorder_using
+  TYPED AS reference_list
+  PRINTED BY pr_firstorder_using_typed
+  RAW_TYPED AS reference_list
+  RAW_PRINTED BY pr_firstorder_using_raw
+  GLOB_TYPED AS reference_list
+  GLOB_PRINTED BY pr_firstorder_using_glob
+| [ "using" reference(a) ] -> [ [a] ]
+| [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
+| [ "using" reference(a) reference(b) reference_list(l) ] -> [
+    Flags.if_verbose
+      Pp.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
+    a::b::l
+  ]
+| [ ] -> [ [] ]
+END
+
 TACTIC EXTEND firstorder
-    [ "firstorder" tactic_opt(t) "using" ne_reference_list(l) ] -> 
-      [ gen_ground_tac true (Option.map eval_tactic t) (Ids l) ]
+    [ "firstorder" tactic_opt(t) firstorder_using(l) ] ->
+      [ gen_ground_tac true (Option.map eval_tactic t) l [] ]
 |   [ "firstorder" tactic_opt(t) "with" ne_preident_list(l) ] -> 
-      [ gen_ground_tac true (Option.map eval_tactic t) (Bases l) ]
+      [ gen_ground_tac true (Option.map eval_tactic t) [] l ]
+|   [ "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) Void ]
+      [ gen_ground_tac true (Option.map eval_tactic t) [] [] ]
 END
 
 TACTIC EXTEND gintuition
   [ "gintuition" tactic_opt(t) ] ->
-     [ gen_ground_tac false (Option.map eval_tactic t) Void ]
+     [ gen_ground_tac false (Option.map eval_tactic t) [] [] ]
 END
 
 
@@ -119,7 +139,7 @@ let default_declarative_automation gls =
        (Some (tclTHEN
 		default_solver
 		(Cctac.congruence_tac !congruence_depth [])))
-       Void) gls
+       [] []) gls
 
 
 
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index fd5972fb7..98b178bde 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -253,17 +253,26 @@ let empty_seq depth=
    history=History.empty;
    depth=depth}
 
-let create_with_ref_list l depth gl=
+let expand_constructor_hints =
+  list_map_append (function
+    | IndRef ind ->
+	list_tabulate (fun i -> ConstructRef (ind,i+1))
+	  (Inductiveops.nconstructors ind)
+    | gr ->
+	[gr])
+
+let extend_with_ref_list l seq gl=
+  let l = expand_constructor_hints l in
   let f gr seq=
     let c=constr_of_global gr in    
     let typ=(pf_type_of gl c) in
       add_formula Hyp gr typ seq gl in
-    List.fold_right f l (empty_seq depth)
+    List.fold_right f l seq
 
 open Auto
 
-let create_with_auto_hints l depth gl=
-  let seqref=ref (empty_seq depth) in
+let extend_with_auto_hints l seq gl=
+  let seqref=ref seq in
   let f p_a_t =
     match p_a_t.code with
 	Res_pf (c,_) | Give_exact c
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 51db9de16..206de27ed 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -57,10 +57,10 @@ val take_formula : t -> Formula.t * t
 
 val empty_seq : int -> t
 
-val create_with_ref_list : global_reference list ->
-  int -> Proof_type.goal sigma -> t
+val extend_with_ref_list : global_reference list ->
+  t -> Proof_type.goal sigma -> t
 
-val create_with_auto_hints : Auto.hint_db_name list -> 
-  int -> Proof_type.goal sigma -> t
+val extend_with_auto_hints : Auto.hint_db_name list -> 
+  t -> Proof_type.goal sigma -> t
 
 val print_cmap: global_reference list CM.t -> unit 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3150ed63b..727fd6f85 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -71,7 +71,6 @@ let substnl_ind_type l n = map_inductive_type (substnl l n)
 let mkAppliedInd (IndType ((ind,params), realargs)) =
   applist (mkInd ind,params@realargs)
 
-
 (* Does not consider imbricated or mutually recursive types *) 
 let mis_is_recursive_subset listind rarg = 
   let rec one_is_rec rvec = 
@@ -125,6 +124,10 @@ let get_full_arity_sign env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_arity_ctxt
 
+let nconstructors ind = 
+  let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
+  Array.length mip.mind_consnames
+
 (* Length of arity (w/o local defs) *)
 
 let inductive_nargs env ind =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index cc1bb7f41..cea769955 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -58,6 +58,8 @@ val mis_nf_constructor_type :
 val mis_constr_nargs : inductive -> int array
 val mis_constr_nargs_env : env -> inductive -> int array
 
+val nconstructors : inductive -> int
+
 (* Return the lengths of parameters signature and real arguments signature *)
 val inductive_nargs : env -> inductive -> int * int
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 394626f24..547ad2a77 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Inductiveops
 open Sign
 open Environ
 open Inductive
@@ -547,10 +548,9 @@ let interp_hints h =
       HintsTransparencyEntry (List.map fr lhints, b)
   | HintsConstructors lqid ->
       let constr_hints_of_ind qid =
-        let isp = global_inductive qid in
-        let consnames = (snd (Global.lookup_inductive isp)).mind_consnames in
-        list_tabulate (fun i -> None, true, mkConstruct (isp,i+1))
-	  (Array.length consnames) in
+        let ind = global_inductive qid in
+        list_tabulate (fun i -> None, true, mkConstruct (ind,i+1))
+	  (nconstructors ind) in
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
       let pat =	Option.map fp patcom in
@@ -727,10 +727,21 @@ let unify_resolve_gen = function
   | None -> unify_resolve_nodelta
   | Some flags -> unify_resolve flags
 
+(* Util *)
+
+let expand_constructor_hints lems =
+  list_map_append (fun lem ->
+    match kind_of_term lem with
+    | Ind ind ->
+	list_tabulate (fun i -> mkConstruct (ind,i+1)) (nconstructors ind)
+    | _ ->
+	[lem]) lems
+
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
 
 let add_hint_lemmas eapply lems hint_db gl =
+  let lems = expand_constructor_hints lems in
   let hintlist' = 
     list_map_append (pf_apply make_resolves gl (eapply,true,false) None) lems in
   Hint_db.add_list hintlist' hint_db
@@ -926,7 +937,7 @@ let extend_local_db gl decl db =
 (* Try to decompose hypothesis [decl] into atomic components of a 
    conjunction with maximum depth [p] (or solve the goal from an 
    empty type) then call the continuation tactic with hint db extended 
-   with the obtappined not-further-decomposable hypotheses *)
+   with the obtained not-further-decomposable hypotheses *)
 
 let rec decomp_and_register_decl p kont (id,_,_ as decl) db gl =
   if p = 0 then