From ef5551e4ca73a93c0820f03ac702ee96e5e7b431 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 30 Sep 2007 19:02:14 +0000
Subject: Ajout infos de débogage de "universe inconsistency" quand option Set 
  Printing Universes est active. Ajout de l'option "using" à la tactique non
 documentée "auto decomp". Ajout de la base "extcore" pour étendre "auto
 decomp" avec des   principes élémentaires tels que le dépliage de "iff".
 Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml  | 24 ++++++++++++------------
 tactics/auto.mli |  4 ++--
 2 files changed, 14 insertions(+), 14 deletions(-)

(limited to 'tactics')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index b78291ecde..f07541912b 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -797,23 +797,23 @@ let h_auto n lems l =
    l'instant *)
 let default_search_decomp = ref 1
 
-let destruct_auto des_opt n gl = 
+let destruct_auto des_opt lems n gl = 
   let hyps = pf_hyps gl in
-  search_gen des_opt n [searchtable_map "core"] 
-    (make_local_hint_db [] gl) hyps gl
+  search_gen des_opt n (List.map searchtable_map ["core";"extcore"])
+    (make_local_hint_db lems gl) hyps gl
     
-let dautomatic des_opt n = tclTRY (destruct_auto des_opt n)
+let dautomatic des_opt lems n = tclTRY (destruct_auto des_opt lems n)
 
-let default_dauto = dautomatic !default_search_decomp !default_search_depth
+let dauto (n,p) lems =
+  let p = match p with Some p -> p | None -> !default_search_decomp in
+  let n = match n with Some n -> n | None -> !default_search_depth in
+  dautomatic p lems n
 
-let dauto = function
-  | None, None     -> default_dauto
-  | Some n, None   -> dautomatic !default_search_decomp n
-  | Some n, Some p -> dautomatic p n
-  | None, Some p   -> dautomatic p !default_search_depth
+let default_dauto = dauto (None,None) []
 
-let h_dauto (n,p) =
-  Refiner.abstract_tactic (TacDAuto (inj_or_var n,p)) (dauto (n,p))
+let h_dauto (n,p) lems =
+  Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map inj_open lems))
+    (dauto (n,p) lems)
 
 (***************************************)
 (*** A new formulation of Auto *********)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 0e702a65b1..ac4f126f38 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -174,11 +174,11 @@ val fmt_autotactic : auto_tactic -> Pp.std_ppcmds
 (*s The following is not yet up to date -- Papageno. *)
 
 (* DAuto *)
-val dauto : int option * int option -> tactic
+val dauto : int option * int option -> constr list -> tactic
 val default_search_decomp : int ref
 val default_dauto : tactic
 
-val h_dauto : int option * int option -> tactic
+val h_dauto : int option * int option -> constr list -> tactic
 (* SuperAuto *)
 
 type autoArguments =
-- 
cgit v1.2.3