summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-02-13 13:48:12 +0000
commit55ce117e8083477593cf1ff2e51a3641c7973830 (patch)
treea82defb4105f175c71b0d13cae42831ce608c4d6 /contrib/subtac/subtac.ml
parent208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff)
Imported Upstream version 8.1+dfsgupstream/8.1+dfsg
Diffstat (limited to 'contrib/subtac/subtac.ml')
-rw-r--r--contrib/subtac/subtac.ml17
1 files changed, 16 insertions, 1 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 26e8f715..5e46bead 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac.ml 9284 2006-10-26 12:06:57Z msozeau $ *)
+(* $Id: subtac.ml 9563 2007-01-31 09:37:18Z msozeau $ *)
open Global
open Pp
@@ -120,6 +120,8 @@ let subtac_end_proof = function
open Pp
open Ppconstr
open Decl_kinds
+open Tacinterp
+open Tacexpr
let start_proof_com env isevars sopt kind (bl,t) hook =
let id = match sopt with
@@ -140,14 +142,27 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+let subtac_utils_path =
+ make_dirpath (List.map id_of_string ["Utils";contrib_name;"Coq"])
+let utils_tac s =
+ lazy(make_kn (MPfile subtac_utils_path) (make_dirpath []) (mk_label s))
+
+let utils_call tac args =
+ TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (utils_tac tac)),args))
+
let start_proof_and_print env isevars idopt k t hook =
start_proof_com env isevars idopt k t hook;
print_subgoals ()
(*if !pcoq <> None then (out_some !pcoq).start_proof ()*)
+let _ = Subtac_obligations.set_default_tactic
+ (Tacinterp.eval_tactic (utils_call "subtac_simpl" []))
+
+
let subtac (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
+ (* check_required_library ["Coq";"Logic";"JMeq"]; *)
require_library "Coq.subtac.FixSub";
require_library "Coq.subtac.Utils";
let env = Global.env () in