summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /contrib/subtac/subtac.ml
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'contrib/subtac/subtac.ml')
-rw-r--r--contrib/subtac/subtac.ml53
1 files changed, 48 insertions, 5 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 84b7d39b..cd2e7c43 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 8688 2006-04-07 15:08:12Z msozeau $ *)
+(* $Id: subtac.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
open Global
open Pp
@@ -48,8 +48,10 @@ let subtac_one_fixpoint env isevars (f, decl) =
let ((id, n, bl, typ, body), decl) =
Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl)
in
- let _ = trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
- Ppconstr.pr_constr_expr body)
+ let _ =
+ try trace (str "Working on a single fixpoint rewritten as: " ++ spc () ++
+ Ppconstr.pr_constr_expr body)
+ with _ -> ()
in ((id, n, bl, typ, body), decl)
@@ -115,16 +117,44 @@ let subtac_end_proof = function
*)
+open Pp
+open Ppconstr
+open Decl_kinds
+
+let start_proof_com env isevars sopt kind (bl,t) hook =
+ let id = match sopt with
+ | Some id ->
+ (* We check existence here: it's a bit late at Qed time *)
+ if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
+ errorlabstrm "start_proof" (pr_id id ++ str " already exists");
+ id
+ | None ->
+ next_global_ident_away false (id_of_string "Unnamed_thm")
+ (Pfedit.get_all_proof_names ())
+ in
+ let evm, c, typ =
+ Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
+ in
+ let _ = Typeops.infer_type env c in
+ Command.start_proof id kind c hook
+
+let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+
+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 (loc, command) =
check_required_library ["Coq";"Init";"Datatypes"];
check_required_library ["Coq";"Init";"Specif"];
require_library "Coq.subtac.FixSub";
require_library "Coq.subtac.Utils";
+ let env = Global.env () in
+ let isevars = ref (create_evar_defs Evd.empty) in
try
match command with
VernacDefinition (defkind, (locid, id), expr, hook) ->
- let env = Global.env () in
- let isevars = ref (create_evar_defs Evd.empty) in
(match expr with
ProveBody (bl, c) ->
let evm, c, ctyp = Subtac_pretyping.subtac_process env isevars id bl c None in
@@ -142,6 +172,19 @@ let subtac (loc, command) =
| VernacFixpoint (l, b) ->
let _ = trace (str "Building fixpoint") in
ignore(Subtac_command.build_recursive l b)
+
+ | VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) ->
+ if not(Pfedit.refining ()) then
+ if lettop then
+ errorlabstrm "Subtac_command.StartProof"
+ (str "Let declarations can only be used in proof editing mode");
+ if Lib.is_modtype () then
+ errorlabstrm "Subtac_command.StartProof"
+ (str "Proof editing mode not supported in module types");
+ start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook
+
+
+
(*| VernacEndProof e ->
subtac_end_proof e*)