diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/command.ml | 4 | ||||
-rw-r--r-- | vernac/command.mli | 3 | ||||
-rw-r--r-- | vernac/lemmas.ml | 10 | ||||
-rw-r--r-- | vernac/lemmas.mli | 17 | ||||
-rw-r--r-- | vernac/obligations.ml | 2 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 43 |
6 files changed, 38 insertions, 41 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index b1425d703..998e7803e 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -187,7 +187,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = let () = definition_message ident in let gr = VarRef ident in let () = maybe_declare_manual_implicits false gr imps in - let () = if Pfedit.refining () then + let () = if Proof_global.there_are_pending_proofs () then warn_definition_not_visible ident in gr @@ -233,7 +233,7 @@ match local with let _ = declare_variable ident decl in let () = assumption_message ident in let () = - if not !Flags.quiet && Pfedit.refining () then + if not !Flags.quiet && Proof_global.there_are_pending_proofs () then Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ strbrk " is not visible from current goals") in diff --git a/vernac/command.mli b/vernac/command.mli index 9bbc2fdac..2a52d9bcb 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -15,7 +15,6 @@ open Vernacexpr open Constrexpr open Decl_kinds open Redexpr -open Pfedit (** This file is about the interpretation of raw commands into typed ones and top-level declaration of the main Gallina objects *) @@ -151,7 +150,7 @@ val declare_fixpoint : locality -> polymorphic -> recursive_preentry * lident list option * Evd.evar_universe_context * (Context.Rel.t * Impargs.manual_implicits * int option) list -> - lemma_possible_guards -> decl_notation list -> unit + Proof_global.lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> recursive_preentry * lident list option * Evd.evar_universe_context * diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 77e356eb2..5bf419caf 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -209,7 +209,7 @@ let compute_proof_name locality = function user_err ?loc (pr_id id ++ str " already exists."); id, pl | None -> - next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None + next_global_ident_away default_thm_id (Proof_global.get_all_proof_names ()), None let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) = let t_i = norm t_i in @@ -487,7 +487,7 @@ let save_proof ?proof = function let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes) | None -> - let pftree = Pfedit.get_pftreestate () in + let pftree = Proof_global.give_me_the_proof () in let id, k, typ = Pfedit.current_proof_statement () in let typ = EConstr.Unsafe.to_constr typ in let universes = Proof.initial_euctx pftree in @@ -496,7 +496,7 @@ let save_proof ?proof = function Proof_global.return_proof ~allow_partial:true () in let sec_vars = if not !keep_admitted_vars then None - else match Pfedit.get_used_variables(), pproofs with + else match Proof_global.get_used_variables(), pproofs with | Some _ as x, _ -> x | None, (pproof, _) :: _ -> let env = Global.env () in @@ -504,7 +504,7 @@ let save_proof ?proof = function let ids_def = Environ.global_vars_set env pproof in Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) | _ -> None in - let names = Pfedit.get_universe_binders () in + let names = Proof_global.get_universe_binders () in let evd = Evd.from_ctx universes in let binders, ctx = Evd.universe_context ?names evd in Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), @@ -519,7 +519,7 @@ let save_proof ?proof = function | Some proof -> proof in (* if the proof is given explicitly, nothing has to be deleted *) - if Option.is_empty proof then Pfedit.delete_current_proof (); + if Option.is_empty proof then Proof_global.discard_current (); Proof_global.(apply_terminator terminator (Proved (is_opaque,idopt,proof_obj))) (* Miscellaneous *) diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli index d06b8fd14..a9c0d99f3 100644 --- a/vernac/lemmas.mli +++ b/vernac/lemmas.mli @@ -9,7 +9,6 @@ open Names open Term open Decl_kinds -open Pfedit type 'a declaration_hook val mk_hook : @@ -21,16 +20,16 @@ val call_hook : (** A hook start_proof calls on the type of the definition being started *) val set_start_hook : (EConstr.types -> unit) -> unit -val start_proof : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> - ?terminator:(lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> +val start_proof : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> + ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> unit declaration_hook -> unit -val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> - ?terminator:(lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> +val start_proof_univs : Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> + ?terminator:(Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> - ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> + ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit val start_proof_com : @@ -40,8 +39,8 @@ val start_proof_com : val start_proof_with_initialization : goal_kind -> Evd.evar_map -> - (bool * lemma_possible_guards * unit Proofview.tactic list option) option -> - ((Id.t (* name of thm *) * universe_binders option) * + (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option -> + ((Id.t (* name of thm *) * Proof_global.universe_binders option) * (types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list -> int list option -> unit declaration_hook -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 6dee95bc5..e03e9b803 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -947,7 +947,7 @@ let rec solve_obligation prg num tac = let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~terminator hook in let _ = Pfedit.by !default_tactic in - Option.iter (fun tac -> Pfedit.set_end_tac tac) tac + Option.iter (fun tac -> Proof_global.set_endline_tactic tac) tac and obligation (user_num, name, typ) tac = let num = pred user_num in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ef16df5b7..5d1def7a4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -15,7 +15,6 @@ open Flags open Names open Nameops open Term -open Pfedit open Tacmach open Constrintern open Prettyp @@ -70,13 +69,13 @@ let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO.") let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) - let pfts = get_pftreestate () in + let pfts = Proof_global.give_me_the_proof () in let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma)) let show_universes () = - let pfts = get_pftreestate () in + let pfts = Proof_global.give_me_the_proof () in let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in @@ -89,7 +88,7 @@ let show_prooftree () = () (* Simulate the Intro(s) tactic *) let show_intro all = let open EConstr in - let pf = get_pftreestate() in + let pf = Proof_global.give_me_the_proof() in let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in if not (List.is_empty gls) then begin let gl = {Evd.it=List.hd gls ; sigma = sigma; } in @@ -508,7 +507,7 @@ let vernac_start_proof locality p kind l lettop = match id with | Some (lid,_) -> Dumpglob.dump_definition lid false "prf" | None -> ()) l; - if not(refining ()) then + if not(Proof_global.there_are_pending_proofs ()) then if lettop then user_err ~hdr:"Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode."); @@ -521,7 +520,7 @@ let vernac_end_proof ?proof = function let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) - let status = by (Tactics.exact_proof c) in + let status = Pfedit.by (Tactics.exact_proof c) in save_proof (Vernacexpr.(Proved(Opaque None,None))); if not status then Feedback.feedback Feedback.AddedAxiom @@ -667,7 +666,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = user_err Pp.(str "Modules and Module Types are not allowed inside sections."); match mexpr_ast_l with | [] -> - check_no_pending_proofs (); + Proof_global.check_no_pending_proof (); let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> @@ -713,7 +712,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = match mty_ast_l with | [] -> - check_no_pending_proofs (); + Proof_global.check_no_pending_proof (); let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> @@ -761,7 +760,7 @@ let vernac_include l = (* Sections *) let vernac_begin_section (_, id as lid) = - check_no_pending_proofs (); + Proof_global.check_no_pending_proof (); Dumpglob.dump_definition lid true "sec"; Lib.open_section id @@ -775,7 +774,7 @@ let vernac_name_sec_hyp (_,id) set = Proof_using.name_set id set (* Dispatcher of the "End" command *) let vernac_end_segment (_,id as lid) = - check_no_pending_proofs (); + Proof_global.check_no_pending_proof (); match Lib.find_opening_node id with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid | Lib.OpenedModule (true,_,_,_) -> vernac_end_modtype lid @@ -855,14 +854,14 @@ let focus_command_cond = Proof.no_cond command_focus there are no more goals to solve. It cannot be a tactic since all tactics fail if there are no further goals to prove. *) -let vernac_solve_existential = instantiate_nth_evar_com +let vernac_solve_existential = Pfedit.instantiate_nth_evar_com let vernac_set_end_tac tac = let env = Genintern.empty_glob_sign (Global.env ()) in let _, tac = Genintern.generic_intern env tac in - if not (refining ()) then + if not (Proof_global.there_are_pending_proofs ()) then user_err Pp.(str "Unknown command of the non proof-editing mode."); - set_end_tac tac + Proof_global.set_endline_tactic tac (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) let vernac_set_used_variables e = @@ -877,13 +876,13 @@ let vernac_set_used_variables e = user_err ~hdr:"vernac_set_used_variables" (str "Unknown variable: " ++ pr_id id)) l; - let _, to_clear = set_used_variables l in + let _, to_clear = Proof_global.set_used_variables l in let to_clear = List.map snd to_clear in Proof_global.with_current_proof begin fun _ p -> if List.is_empty to_clear then (p, ()) else let tac = Tactics.clear to_clear in - fst (solve SelectAll None tac p), () + fst (Pfedit.solve SelectAll None tac p), () end (*****************************) @@ -927,12 +926,12 @@ let vernac_chdir = function (* State management *) let vernac_write_state file = - Pfedit.delete_all_proofs (); + Proof_global.discard_all (); let file = CUnix.make_suffix file ".coq" in States.extern_state file let vernac_restore_state file = - Pfedit.delete_all_proofs (); + Proof_global.discard_all (); let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in States.intern_state file @@ -1526,7 +1525,7 @@ let vernac_print_option key = with Not_found -> error_undeclared_key key let get_current_context_of_args = function - | Some n -> get_goal_context n + | Some n -> Pfedit.get_goal_context n | None -> get_current_context () let query_command_selector ?loc = function @@ -1588,7 +1587,7 @@ let vernac_global_check c = let get_nth_goal n = - let pf = get_pftreestate() in + let pf = Proof_global.give_me_the_proof() in let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in gl @@ -1777,7 +1776,7 @@ let vernac_locate = let open Feedback in function | LocateFile f -> msg_notice (locate_file f) let vernac_register id r = - if Pfedit.refining () then + if Proof_global.there_are_pending_proofs () then user_err Pp.(str "Cannot register a primitive while in proof editing mode."); let kn = Constrintern.global_reference (snd id) in if not (isConstRef kn) then @@ -1854,14 +1853,14 @@ let vernac_show = let open Feedback in function | ShowUniverses -> show_universes () | ShowTree -> show_prooftree () | ShowProofNames -> - msg_notice (pr_sequence pr_id (Pfedit.get_all_proof_names())) + msg_notice (pr_sequence pr_id (Proof_global.get_all_proof_names())) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id | ShowThesis -> show_thesis () let vernac_check_guard () = - let pts = get_pftreestate () in + let pts = Proof_global.give_me_the_proof () in let pfterm = List.hd (Proof.partial_proof pts) in let message = try |