- 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

3 files changed, 54 insertions, 25 deletions

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