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

13 files changed, 139 insertions, 88 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 128adb607..21f977f1c 100755
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -337,7 +337,7 @@ let e_breadth_search debug n db_list local_db gl =
   with Not_found -> error "EAuto: breadth first search failed"
 
 let e_search_auto debug (n,p) db_list gl = 
-  let local_db = make_local_hint_db gl in 
+  let local_db = make_local_hint_db [] gl in 
   if n = 0 then 
     e_depth_search debug p db_list local_db gl
   else 
@@ -357,7 +357,7 @@ let full_eauto debug n gl =
   let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
-  let _local_db = make_local_hint_db gl in
+  let _local_db = make_local_hint_db [] gl in
   tclTRY (e_search_auto debug n db_list) gl
 
 let my_full_eauto n gl = full_eauto false (n,0) gl
@@ -497,7 +497,7 @@ let full_auto n gl =
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+  tclTRY (search n db_list (make_local_hint_db [] gl) hyps) gl
   
 let default_full_auto gl = full_auto !default_search_depth gl
 (************************************************************************)
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 85fbea50c..ea7b52162 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1030,14 +1030,16 @@ and xlate_tac =
         (if a3 then CT_destructing else CT_coerce_NONE_to_DESTRUCTING CT_none),
         (if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none))
     | TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt)
-    | TacAuto (nopt, Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
-    | TacAuto (nopt, None) ->
+    | TacAuto (nopt, [], Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt)
+    | TacAuto (nopt, [], None) ->
  	CT_auto_with (xlate_int_or_var_opt_to_int_opt nopt,
 		      CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
-    | TacAuto (nopt, Some (id1::idl)) ->
+    | TacAuto (nopt, [], Some (id1::idl)) ->
 	CT_auto_with(xlate_int_or_var_opt_to_int_opt nopt,
              CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
              CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl)))
+    | TacAuto (nopt, _::_, _) ->
+	xlate_error "TODO: auto using"
     |TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) ->
        let (id_list:ct_ID list) =
 	 List.map (fun x -> CT_ident x) (out_gen (wit_list1 rawwit_pre_ident) l) in
@@ -1051,7 +1053,7 @@ and xlate_tac =
 	   | [] -> CT_coerce_NONE_to_TACTIC_OPT CT_none
 	   | _ -> assert false in
 	 CT_autorewrite (CT_id_ne_list(fst, id_list1), t1)
-    | TacExtend (_,"eauto", [nopt; popt; idl]) ->
+    | TacExtend (_,"eauto", [nopt; popt; lems; idl]) ->
 	let first_n =
 	  match out_gen (wit_opt rawwit_int_or_var) nopt with
 	    | Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
@@ -1062,6 +1064,10 @@ and xlate_tac =
 	    | Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
 	    | Some ArgArg n -> xlate_int_to_id_or_int_opt n
 	    | None -> none_in_id_or_int_opt in
+	let _lems =
+	  match out_gen Eauto.rawwit_auto_using lems with
+	    | [] -> []
+	    | _ -> xlate_error "TODO: eauto using" in
 	let idl = out_gen Eauto.rawwit_hintbases idl in
           (match idl with
 	    None -> CT_eauto_with(first_n,
@@ -1083,12 +1089,14 @@ and xlate_tac =
      let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in
      let c = xlate_formula c and bindl = xlate_bindings bindl in
      CT_eapply (c, bindl)
-    | TacTrivial (Some []) -> CT_trivial
-    | TacTrivial None -> 
+    | TacTrivial ([],Some []) -> CT_trivial
+    | TacTrivial ([],None) -> 
 	CT_trivial_with(CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star)
-    | TacTrivial (Some (id1::idl)) ->
+    | TacTrivial ([],Some (id1::idl)) ->
 	 CT_trivial_with(CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
             (CT_id_ne_list(CT_ident id1,List.map (fun x -> CT_ident x) idl))))
+    | TacTrivial (_::_,_) ->
+	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
     | TacApply (c,bindl) ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a4491fbef..94d185211 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 d9ef227f6..8e8413de4 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 fd448281f..7b546b290 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 e4bc4549b..6d27c274c 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) ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 5da2f2a30..c487c34a0 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -152,8 +152,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacLApply of 'constr
 
   (* Automation tactics *)
-  | TacTrivial of string list option
-  | TacAuto of int or_var option * string list option
+  | TacTrivial of 'constr list * string list option
+  | TacAuto of int or_var option * 'constr list * string list option
   | TacAutoTDB of int option
   | TacDestructHyp of (bool * identifier located)
   | TacDestructConcl
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 3aaf3443e..edda5c25b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -567,11 +567,11 @@ let unify_resolve (c,clenv) gls =
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
 
-let make_local_hint_db g = 
+let make_local_hint_db lems g =
   let sign = pf_hyps g in
-  let hintlist = list_map_append (make_resolve_hyp (pf_env g) (project g)) sign
-  in Hint_db.add_list hintlist Hint_db.empty
-
+  let hintlist = list_map_append (pf_apply make_resolve_hyp g) sign in
+  let hintlist' = list_map_append (pf_apply make_resolves g true) lems in
+  Hint_db.add_list hintlist' (Hint_db.add_list hintlist Hint_db.empty)
 
 (* Serait-ce possible de compiler d'abord la tactique puis de faire la
    substitution sans passer par bdize dont l'objectif est de préparer un
@@ -648,7 +648,7 @@ and trivial_resolve db_list local_db cl =
   with Bound | Not_found -> 
     []
 
-let trivial dbnames gl =
+let trivial lems dbnames gl =
   let db_list = 
     List.map
       (fun x -> 
@@ -658,19 +658,20 @@ let trivial dbnames gl =
 	   error ("trivial: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
-  tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
+  tclTRY (trivial_fail_db db_list (make_local_hint_db lems gl)) gl 
     
-let full_trivial gl =
+let full_trivial lems gl =
   let dbnames = Hintdbmap.dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
-  tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl
+  tclTRY (trivial_fail_db db_list (make_local_hint_db lems gl)) gl
 
-let gen_trivial = function
-  | None -> full_trivial
-  | Some l -> trivial l
+let gen_trivial lems = function
+  | None -> full_trivial lems
+  | Some l -> trivial lems l
 
-let h_trivial l = Refiner.abstract_tactic (TacTrivial l) (gen_trivial l)
+let h_trivial lems l =
+  Refiner.abstract_tactic (TacTrivial (lems,l)) (gen_trivial lems l)
 
 (**************************************************************************)
 (*                       The classical Auto tactic                        *)
@@ -746,8 +747,8 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 let search = search_gen 0
 
 let default_search_depth = ref 5
-			     
-let auto n dbnames gl = 
+
+let auto n lems dbnames gl =
   let db_list = 
     List.map
       (fun x -> 
@@ -758,29 +759,29 @@ let auto n dbnames gl =
       ("core"::dbnames) 
   in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+  tclTRY (search n db_list (make_local_hint_db lems gl) hyps) gl
 
-let default_auto = auto !default_search_depth []
+let default_auto = auto !default_search_depth [] []
 
-let full_auto n gl = 
+let full_auto n lems gl = 
   let dbnames = Hintdbmap.dom !searchtable in
   let dbnames = list_subtract dbnames ["v62"] in
   let db_list = List.map (fun x -> searchtable_map x) dbnames in
   let hyps = pf_hyps gl in
-  tclTRY (search n db_list (make_local_hint_db gl) hyps) gl
+  tclTRY (search n db_list (make_local_hint_db lems gl) hyps) gl
   
-let default_full_auto gl = full_auto !default_search_depth gl
+let default_full_auto gl = full_auto !default_search_depth [] gl
 
-let gen_auto n dbnames =
+let gen_auto n lems dbnames =
   let n = match n with None -> !default_search_depth | Some n -> n in
   match dbnames with
-  | None -> full_auto n
-  | Some l -> auto n l
+  | None -> full_auto n lems
+  | Some l -> auto n lems l
 
 let inj_or_var = option_app (fun n -> Genarg.ArgArg n)
 
-let h_auto n l =
-  Refiner.abstract_tactic (TacAuto (inj_or_var n,l)) (gen_auto n l)
+let h_auto n lems l =
+  Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l)
 
 (**************************************************************************)
 (*                  The "destructing Auto" from Eduardo                   *)
@@ -795,7 +796,7 @@ let default_search_decomp = ref 1
 let destruct_auto des_opt n gl = 
   let hyps = pf_hyps gl in
   search_gen des_opt n [searchtable_map "core"] 
-    (make_local_hint_db gl) hyps gl
+    (make_local_hint_db [] gl) hyps gl
     
 let dautomatic des_opt n = tclTRY (destruct_auto des_opt n)
 
@@ -880,7 +881,7 @@ let search_superauto n to_add argl g =
       (fun (id,c) -> add_named_decl (id, None, pf_type_of g c))
       to_add empty_named_context in
   let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in
-  let db = Hint_db.add_list db0 (make_local_hint_db g) in
+  let db = Hint_db.add_list db0 (make_local_hint_db [] g) in
   super_search n [Hintdbmap.find "core" !searchtable] db argl g
 
 let superauto n to_add argl  = 
diff --git a/tactics/auto.mli b/tactics/auto.mli
index ee638499f..0e702a65b 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -127,7 +127,7 @@ val set_extern_subst_tactic :
 (* Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints *)
 
-val make_local_hint_db : goal sigma -> Hint_db.t
+val make_local_hint_db : constr list -> goal sigma -> Hint_db.t
 
 val priority : (int * 'a) list -> 'a list
 
@@ -145,29 +145,29 @@ val conclPattern : constr -> constr_pattern -> Tacexpr.glob_tactic_expr -> tacti
 
 (* The Auto tactic *)
 
-val auto : int -> hint_db_name list -> tactic
+val auto : int -> constr list -> hint_db_name list -> tactic
 
 (* auto with default search depth and with the hint database "core" *)
 val default_auto : tactic
 
 (* auto with all hint databases except the "v62" compatibility database *)
-val full_auto : int -> tactic
+val full_auto : int -> constr list -> tactic
 
 (* auto with default search depth and with all hint databases 
    except the "v62" compatibility database *)
 val default_full_auto : tactic
 
 (* The generic form of auto (second arg [None] means all bases) *)
-val gen_auto : int option -> hint_db_name list option -> tactic
+val gen_auto : int option -> constr list -> hint_db_name list option -> tactic
 
 (* The hidden version of auto *)
-val h_auto   : int option -> hint_db_name list option -> tactic
+val h_auto   : int option -> constr list -> hint_db_name list option -> tactic
 
 (* Trivial *)
-val trivial : hint_db_name list -> tactic
-val gen_trivial : hint_db_name list option -> tactic
-val full_trivial : tactic
-val h_trivial : hint_db_name list option -> tactic
+val trivial : constr list -> hint_db_name list -> tactic
+val gen_trivial : constr list -> hint_db_name list option -> tactic
+val full_trivial : constr list -> tactic
+val h_trivial : constr list -> hint_db_name list option -> tactic
 
 val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index d92c4f2ed..fd1f38786 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -354,14 +354,14 @@ let e_breadth_search debug n db_list local_db gl =
     s.SearchProblem.tacres
   with Not_found -> error "EAuto: breadth first search failed"
 
-let e_search_auto debug (in_depth,p) db_list gl = 
-  let local_db = make_local_hint_db gl in 
+let e_search_auto debug (in_depth,p) lems db_list gl = 
+  let local_db = make_local_hint_db lems gl in 
   if in_depth then 
     e_depth_search debug p db_list local_db gl
   else 
     e_breadth_search debug p db_list local_db gl
 
-let eauto debug np dbnames = 
+let eauto debug np lems dbnames =
   let db_list =
     List.map
       (fun x -> 
@@ -369,18 +369,17 @@ let eauto debug np dbnames =
 	 with Not_found -> error ("EAuto: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
-  tclTRY (e_search_auto debug np db_list)
+  tclTRY (e_search_auto debug np lems db_list)
 
-let full_eauto debug n gl = 
+let full_eauto debug n lems gl = 
   let dbnames = current_db_names () in
   let dbnames =  list_subtract dbnames ["v62"] in
   let db_list = List.map searchtable_map dbnames in
-  let local_db = make_local_hint_db gl in
-  tclTRY (e_search_auto debug n db_list) gl
+  tclTRY (e_search_auto debug n lems db_list) gl
 
-let gen_eauto d np = function
-  | None -> full_eauto d np
-  | Some l -> eauto d np l
+let gen_eauto d np lems = function
+  | None -> full_eauto d np lems
+  | Some l -> eauto d np lems l
 
 let make_depth = function
   | None -> !default_search_depth 
@@ -396,10 +395,7 @@ open Genarg
 
 (* Hint bases *)
 
-let pr_hintbases _prc _prlc _prt = function 
-  | None -> str " with *"
-  | Some [] -> mt ()
-  | Some l -> str " with " ++ Util.prlist_with_sep spc str l
+let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
 
 ARGUMENT EXTEND hintbases
   TYPED AS preident_list_opt
@@ -409,7 +405,26 @@ ARGUMENT EXTEND hintbases
 | [ ] -> [ Some [] ]
 END
 
+let pr_constr_coma_sequence prc _ _ = prlist_with_sep pr_coma prc
+
+ARGUMENT EXTEND constr_coma_sequence
+  TYPED AS constr_list
+  PRINTED BY pr_constr_coma_sequence
+| [ constr(c) "," constr_coma_sequence(l) ] -> [ c::l ]
+| [ constr(c) ] -> [ [c] ]
+END
+
+let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+
+ARGUMENT EXTEND auto_using
+  TYPED AS constr_list
+  PRINTED BY pr_auto_using
+| [ "using" constr_coma_sequence(l) ] -> [ l ]
+| [ ] -> [ [] ]
+END
+
 TACTIC EXTEND eauto
-| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) hintbases(db) ] ->
-    [ gen_eauto false (make_dimension n p) db ]
+| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) 
+    hintbases(db) ] ->
+    [ gen_eauto false (make_dimension n p) lems db ]
 END
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 57f6a4171..4621088e2 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -11,10 +11,13 @@ open Term
 open Proof_type
 open Tacexpr
 open Auto
+open Topconstr
 (*i*)
 
 val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
 
+val rawwit_auto_using : constr_expr list raw_abstract_argument_type
+
 val e_assumption : tactic
 
 val registered_e_assumption : tactic
@@ -25,5 +28,6 @@ val vernac_e_resolve_constr :  constr -> tactic
 
 val e_give_exact_constr : constr -> tactic
 
-val gen_eauto : bool -> bool * int -> hint_db_name list option -> tactic
+val gen_eauto : bool -> bool * int -> constr list -> 
+  hint_db_name list option -> tactic
 
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 1ef4b928d..4bd83c672 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -114,7 +114,7 @@ let diseqCase =
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (h_simplest_apply (mkVar diseq))
   (tclTHEN  (Extratactics.h_injHyp (Rawterm.NamedHyp absurd))
-            full_trivial))))))
+            (full_trivial [])))))))
 
 let solveArg a1 a2 tac  g = 
   let rectype = pf_type_of g a1 in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 476332bda..7eff2b69f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -234,8 +234,8 @@ let _ =
         "intros", TacIntroPattern [];
         "assumption", TacAssumption;
         "cofix", TacCofix None;
-        "trivial", TacTrivial None;
-        "auto", TacAuto(None,None);
+        "trivial", TacTrivial ([],None);
+        "auto", TacAuto(None,[],None);
         "left", TacLeft NoBindings;
         "right", TacRight NoBindings;
         "split", TacSplit(false,NoBindings);
@@ -655,8 +655,10 @@ let rec intern_atomic lf ist x =
 *)
 
   (* Automation tactics *)
-  | TacTrivial l -> TacTrivial l
-  | TacAuto (n,l) -> TacAuto (option_app (intern_int_or_var ist) n,l)
+  | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
+  | TacAuto (n,lems,l) ->
+      TacAuto (option_app (intern_int_or_var ist) n,
+        List.map (intern_constr ist) lems,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
   | TacDestructConcl -> TacDestructConcl
@@ -1750,9 +1752,12 @@ and interp_atomic ist gl = function
 	     HypLocation(interp_hyp ist gl id,hloc))
 *)
   (* Automation tactics *)
-  | TacTrivial l -> Auto.h_trivial (option_app (List.map (interp_hint_base ist)) l)
-  | TacAuto (n, l) ->
+  | TacTrivial (lems,l) -> 
+      Auto.h_trivial (List.map (pf_interp_constr ist gl) lems)
+	(option_app (List.map (interp_hint_base ist)) l)
+  | TacAuto (n,lems,l) ->
       Auto.h_auto (option_app (interp_int_or_var ist) n)
+      (List.map (pf_interp_constr ist gl) lems)
       (option_app (List.map (interp_hint_base ist)) l)
   | TacAutoTDB n -> Dhyp.h_auto_tdb n
   | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
@@ -2012,8 +2017,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
 (*| TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido)
 *)
   (* Automation tactics *)
-  | TacTrivial l -> TacTrivial l
-  | TacAuto (n,l) -> TacAuto (n,l)
+  | TacTrivial (lems,l) -> TacTrivial (List.map (subst_rawconstr subst) lems,l)
+  | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_rawconstr subst) lems,l)
   | TacAutoTDB n -> TacAutoTDB n
   | TacDestructHyp (b,id) -> TacDestructHyp(b,id)
   | TacDestructConcl -> TacDestructConcl