diff options
| -rw-r--r-- | contrib/first-order/g_ground.ml4 | 52 | ||||
| -rw-r--r-- | contrib/first-order/sequent.ml | 11 | ||||
| -rw-r--r-- | contrib/first-order/sequent.mli | 3 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 2 |
4 files changed, 43 insertions, 25 deletions
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4 index 95488265b5..da1d0dcbdd 100644 --- a/contrib/first-order/g_ground.ml4 +++ b/contrib/first-order/g_ground.ml4 @@ -18,6 +18,7 @@ open Tactics open Tacticals open Term open Names +open Libnames (* declaring search depth as a global option *) @@ -40,7 +41,12 @@ let default_solver=(Tacinterp.interp <:tactic<Auto with *>>) let fail_solver=tclFAIL 0 "GTauto failed" -let gen_ground_tac flag taco l gl= +type external_env= + Ids of global_reference list + | Bases of Auto.hint_db_name list + | Void + +let gen_ground_tac flag taco ext gl= let backup= !qflag in try qflag:=flag; @@ -48,12 +54,16 @@ let gen_ground_tac flag taco l gl= match taco with Some tac->tac | None-> default_solver in - let startseq=create_with_ref_list l !ground_depth in + let startseq= + match ext with + Void -> (fun gl -> empty_seq !ground_depth) + | Ids l-> create_with_ref_list l !ground_depth + | Bases l-> create_with_auto_hints l !ground_depth in let result=ground_tac solver startseq gl in qflag:=backup;result with e ->qflag:=backup;raise e - -(* special for compatibility with old Intuition *) + +(* special for compatibility with old Intuition let constant str = Coqlib.gen_constant "User" ["Init";"Logic"] str @@ -67,30 +77,32 @@ let normalize_evaluables= None->unfold_in_concl (Lazy.force defined_connectives) | Some id-> unfold_in_hyp (Lazy.force defined_connectives) - (Tacexpr.InHypType id)) + (Tacexpr.InHypType id)) *) TACTIC EXTEND Ground - | [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> - [ gen_ground_tac true (Some (snd t)) l ] - | [ "Ground" tactic(t) ] -> - [ gen_ground_tac true (Some (snd t)) [] ] - | [ "Ground" "with" ne_reference_list(l) ] -> - [ gen_ground_tac true None l ] - | [ "Ground" ] -> - [ gen_ground_tac true None [] ] + [ "Ground" tactic(t) "with" ne_reference_list(l) ] -> + [ gen_ground_tac true (Some (snd t)) (Ids l) ] +| [ "Ground" "with" ne_reference_list(l) ] -> + [ gen_ground_tac true None (Ids l) ] +| [ "Ground" tactic(t) "using" ne_preident_list(l) ] -> + [ gen_ground_tac true (Some (snd t)) (Bases l) ] +| [ "Ground" "using" ne_preident_list(l) ] -> + [ gen_ground_tac true None (Bases l) ] +| [ "Ground" tactic(t) ] -> + [ gen_ground_tac true (Some (snd t)) Void ] +| [ "Ground" ] -> + [ gen_ground_tac true None Void ] END TACTIC EXTEND GTauto - [ "GTauto" ] -> - [ gen_ground_tac false (Some fail_solver) [] ] + [ "Tauto" ] -> + [ gen_ground_tac false (Some fail_solver) Void ] END TACTIC EXTEND GIntuition - ["GIntuition" tactic(t)] -> - [ gen_ground_tac false - (Some(tclTHEN normalize_evaluables (snd t))) [] ] + [ "GIntuition" tactic(t) ] -> + [ gen_ground_tac false (Some (snd t)) Void ] | [ "GIntuition" ] -> - [ gen_ground_tac false - (Some (tclTHEN normalize_evaluables default_solver)) [] ] + [ gen_ground_tac false (Some default_solver) Void ] END diff --git a/contrib/first-order/sequent.ml b/contrib/first-order/sequent.ml index 4d074f67f1..a91b4956c8 100644 --- a/contrib/first-order/sequent.ml +++ b/contrib/first-order/sequent.ml @@ -258,7 +258,7 @@ let create_with_ref_list l depth gl= open Auto -let create_with_auto_hints depth gl= +let create_with_auto_hints l depth gl= let seqref=ref (empty_seq depth) in let f p_a_t = match p_a_t.code with @@ -271,8 +271,13 @@ let create_with_auto_hints depth gl= with Not_found->()) | _-> () in let g _ l=List.iter f l in - let h str hdb=Hint_db.iter g hdb in - Util.Stringmap.iter h (!searchtable); + let h dbname= + let hdb= + try + Util.Stringmap.find dbname !searchtable + with Not_found-> error ("Ground: "^dbname^" : No such Hint database") in + Hint_db.iter g hdb in + List.iter h l; !seqref let print_cmap map= diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli index 26c3a95bd7..b126bf638e 100644 --- a/contrib/first-order/sequent.mli +++ b/contrib/first-order/sequent.mli @@ -60,6 +60,7 @@ val empty_seq : int -> t val create_with_ref_list : global_reference list -> int -> Proof_type.goal sigma -> t -val create_with_auto_hints : int -> Proof_type.goal sigma -> t +val create_with_auto_hints : Auto.hint_db_name list -> + int -> Proof_type.goal sigma -> t val print_cmap: global_reference list CM.t -> unit diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index c8740b9302..36a98a4aa0 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -189,7 +189,7 @@ let lfo_wrap n gl= errorlabstrm "LinearIntuition" [< str "LinearIntuition failed." >] TACTIC EXTEND Tauto -| [ "Tauto" ] -> [ tauto ] +| [ "OldTauto" ] -> [ tauto ] END TACTIC EXTEND TSimplif |