diff options
Diffstat (limited to 'contrib/subtac/subtac.ml')
| -rw-r--r-- | contrib/subtac/subtac.ml | 53 |
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*) |