- 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

1 files changed, 13 insertions, 4 deletions

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