Ajout option 'using lemmas' à auto/trivial/eauto

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

4 files changed, 33 insertions, 15 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a4491fbef4..94d185211b 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -274,6 +274,10 @@ GEXTEND Gram
       | "with"; l = LIST1 IDENT -> Some l
       | -> Some [] ] ]
   ;
+  auto_using:
+    [ [ "using"; l = LIST1 constr SEP "," -> l
+      | -> [] ] ]
+  ;
   eliminator:
     [ [ "using"; el = constr_with_bindings -> el ] ]
   ;
@@ -367,8 +371,10 @@ GEXTEND Gram
         -> TacDecompose (l,c)
 
       (* Automation tactic *)
-      | IDENT "trivial"; db = hintbases -> TacTrivial db
-      | IDENT "auto"; n = OPT int_or_var; db = hintbases -> TacAuto (n, db)
+      | IDENT "trivial"; lems = auto_using; db = hintbases ->
+	  TacTrivial (lems,db)
+      | IDENT "auto"; n = OPT int_or_var; lems = auto_using; db = hintbases ->
+	  TacAuto (n,lems,db)
 
 (* Obsolete since V8.0
       | IDENT "autotdb"; n = OPT natural -> TacAutoTDB n
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index d9ef227f69..8e8413de45 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -487,6 +487,11 @@ let pr_hintbases = function
   | Some l ->
       spc () ++ hov 2 (str "with" ++ prlist (fun s -> spc () ++ str s) l)
 
+let pr_auto_using prc = function
+  | [] -> mt ()
+  | l -> spc () ++ 
+      hov 2 (str "using" ++ spc () ++ prlist_with_sep pr_coma prc l)
+
 let pr_autoarg_adding = function
   | [] -> mt ()
   | l ->
@@ -599,8 +604,8 @@ let rec pr_atom0 env = function
   | TacIntroMove (None,None) -> str "intro"
   | TacAssumption -> str "assumption"
   | TacAnyConstructor None -> str "constructor"
-  | TacTrivial (Some []) -> str "trivial"
-  | TacAuto (None,Some []) -> str "auto"
+  | TacTrivial ([],Some []) -> str "trivial"
+  | TacAuto (None,[],Some []) -> str "auto"
   | TacReflexivity -> str "reflexivity"
   | t -> str "(" ++ pr_atom1 env t ++ str ")"
 
@@ -708,11 +713,14 @@ and pr_atom1 env = function
       hov 1 (str "lapply" ++ pr_constrarg env c)
 
   (* Automation tactics *)
-  | TacTrivial (Some []) as x -> pr_atom0 env x
-  | TacTrivial db -> hov 0 (str "trivial" ++ pr_hintbases db)
-  | TacAuto (None,Some []) as x -> pr_atom0 env x
-  | TacAuto (n,db) ->
-      hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++ pr_hintbases db)
+  | TacTrivial ([],Some []) as x -> pr_atom0 env x
+  | TacTrivial (lems,db) ->
+      hov 0 (str "trivial" ++ 
+             pr_auto_using (pr_constr env) lems ++ pr_hintbases db)
+  | TacAuto (None,[],Some []) as x -> pr_atom0 env x
+  | TacAuto (n,lems,db) ->
+      hov 0 (str "auto" ++ pr_opt (pr_or_var int) n ++ 
+             pr_auto_using (pr_constr env) lems ++ pr_hintbases db)
   | TacDAuto (n,p) ->
       hov 1 (str "auto" ++ pr_opt (pr_or_var int) n ++ str "decomp" ++ pr_opt int p)
 
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index fd448281f6..7b546b2906 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -84,3 +84,7 @@ val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds
 val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
 
 val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds
+
+val pr_hintbases : string list option -> std_ppcmds
+
+val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index e4bc4549bc..6d27c274cd 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -371,15 +371,15 @@ let rec mlexpr_of_atomic_tactic = function
   | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_constr c$ >>
 
   (* Automation tactics *)
-  | Tacexpr.TacAuto (n,l) ->
+  | Tacexpr.TacAuto (n,lems,l) ->
       let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in
+      let lems = mlexpr_of_list mlexpr_of_constr lems in
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
-      <:expr< Tacexpr.TacAuto $n$ $l$ >>
-(*
-  | Tacexpr.TacTrivial l ->
+      <:expr< Tacexpr.TacAuto $n$ $lems$ $l$ >>
+  | Tacexpr.TacTrivial (lems,l) ->
       let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in
-      <:expr< Tacexpr.TacTrivial $l$ >>
-*)
+      let lems = mlexpr_of_list mlexpr_of_constr lems in
+      <:expr< Tacexpr.TacTrivial $lems$ $l$ >>
 
 (*
   | Tacexpr.TacExtend (s,l) ->