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

2 files changed, 18 insertions, 10 deletions

diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 128adb6073..21f977f1c0 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 85fbea50cf..ea7b521624 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) ->