diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 24 | ||||
| -rw-r--r-- | proofs/proof.mli | 5 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 99 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 45 |
4 files changed, 25 insertions, 148 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 1aeb24606b..4ce932b93d 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -351,19 +351,13 @@ let dependent_start ~name ~poly goals = type open_error_reason = | UnfinishedProof - | HasShelvedGoals | HasGivenUpGoals - | HasUnresolvedEvar let print_open_error_reason er = let open Pp in match er with | UnfinishedProof -> str "Attempt to save an incomplete proof" - | HasShelvedGoals -> - str "Attempt to save a proof with shelved goals" | HasGivenUpGoals -> strbrk "Attempt to save a proof with given up goals. If this is really what you want to do, use Admitted in place of Qed." - | HasUnresolvedEvar -> - strbrk "Attempt to save a proof with existential variables still non-instantiated" exception OpenProof of Names.Id.t option * open_error_reason @@ -375,19 +369,25 @@ let _ = CErrors.register_handler begin function | _ -> raise CErrors.Unhandled end +let warn_remaining_shelved_goals = + CWarnings.create ~name:"remaining-shelved-goals" ~category:"tactics" + (fun () -> Pp.str"The proof has remaining shelved goals") + +let warn_remaining_unresolved_evars = + CWarnings.create ~name:"remaining-unresolved-evars" ~category:"tactics" + (fun () -> Pp.str"The proof has unresolved variables") + let return ?pid (p : t) = if not (is_done p) then raise (OpenProof(pid, UnfinishedProof)) - else if has_shelved_goals p then - raise (OpenProof(pid, HasShelvedGoals)) else if has_given_up_goals p then raise (OpenProof(pid, HasGivenUpGoals)) - else if has_unresolved_evar p then - (* spiwack: for compatibility with <= 8.3 proof engine *) - raise (OpenProof(pid, HasUnresolvedEvar)) - else + else begin + if has_shelved_goals p then warn_remaining_shelved_goals () + else if has_unresolved_evar p then warn_remaining_unresolved_evars (); let p = unfocus end_of_stack_kind p () in Proofview.return p.proofview + end let compact p = let entry, proofview = Proofview.compact p.entry p.proofview in diff --git a/proofs/proof.mli b/proofs/proof.mli index fd5e905a3b..40e8ff7eef 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -130,13 +130,10 @@ val compact : t -> t (* Returns the proofs (with their type) of the initial goals. Raises [UnfinishedProof] is some goals remain to be considered. Raises [HasShelvedGoals] if some goals are left on the shelf. - Raises [HasGivenUpGoals] if some goals have been given up. - Raises [HasUnresolvedEvar] if some evars have been left undefined. *) + Raises [HasGivenUpGoals] if some goals have been given up. *) type open_error_reason = | UnfinishedProof - | HasShelvedGoals | HasGivenUpGoals - | HasUnresolvedEvar exception OpenProof of Names.Id.t option * open_error_reason diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f8adc58921..9ee9e7ae2c 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -22,51 +22,6 @@ open Names module NamedDecl = Context.Named.Declaration -(*** Proof Modes ***) - -(* Type of proof modes : - - A function [set] to set it *from standard mode* - - A function [reset] to reset the *standard mode* from it *) -type proof_mode_name = string -type proof_mode = { - name : proof_mode_name ; - set : unit -> unit ; - reset : unit -> unit -} - -let proof_modes = Hashtbl.create 6 -let find_proof_mode n = - try Hashtbl.find proof_modes n - with Not_found -> - CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." n)) - -let register_proof_mode ({name = n} as m) = - Hashtbl.add proof_modes n (CEphemeron.create m) - -(* initial mode: standard mode *) -let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) } -let _ = register_proof_mode standard - -(* Default proof mode, to be set at the beginning of proofs. *) -let default_proof_mode = ref (find_proof_mode "No") - -let get_default_proof_mode_name () = - (CEphemeron.default !default_proof_mode standard).name - -let proof_mode_opt_name = ["Default";"Proof";"Mode"] -let () = - Goptions.(declare_string_option { - optdepr = false; - optname = "default proof mode" ; - optkey = proof_mode_opt_name ; - optread = begin fun () -> - (CEphemeron.default !default_proof_mode standard).name - end; - optwrite = begin fun n -> - default_proof_mode := find_proof_mode n - end - }) - (*** Proof Global Environment ***) (* Extra info on proofs. *) @@ -95,7 +50,6 @@ type pstate = { endline_tactic : Genarg.glob_generic_argument option; section_vars : Constr.named_context option; proof : Proof.t; - mode : proof_mode CEphemeron.key; universe_decl: UState.universe_decl; strength : Decl_kinds.goal_kind; } @@ -109,23 +63,8 @@ let apply_terminator f = f to be resumed when the current proof is closed or aborted. *) let pstates = ref ([] : pstate list) -(* Current proof_mode, for bookkeeping *) -let current_proof_mode = ref !default_proof_mode - -(* combinators for proof modes *) -let update_proof_mode () = - match !pstates with - | { mode = m } :: _ -> - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); - current_proof_mode := m; - CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ()) - | _ -> - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()); - current_proof_mode := find_proof_mode "No" - (* combinators for the current_proof lists *) -let push a l = l := a::!l; - update_proof_mode () +let push a l = l := a::!l exception NoSuchProof let () = CErrors.register_handler begin function @@ -221,25 +160,8 @@ let discard {CAst.loc;v=id} = let discard_current () = if List.is_empty !pstates then raise NoCurrentProof else pstates := List.tl !pstates - let discard_all () = pstates := [] -(* [set_proof_mode] sets the proof mode to be used after it's called. It is - typically called by the Proof Mode command. *) -let set_proof_mode m id = - pstates := List.map - (fun ps -> if pf_name_eq id ps then { ps with mode = m } else ps) - !pstates; - update_proof_mode () - -let set_proof_mode mn = - set_proof_mode (find_proof_mode mn) (get_current_proof_name ()) - -let activate_proof_mode mode = - CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ()) -let disactivate_current_proof_mode () = - CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ()) - (** [start_proof sigma id pl str goals terminator] starts a proof of name [id] with goals [goals] (a list of pairs of environment and conclusion); [str] describes what kind of theorem/definition this @@ -254,9 +176,8 @@ let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals terminator proof = Proof.start ~name ~poly:(pi2 kind) sigma goals; endline_tactic = None; section_vars = None; - mode = find_proof_mode "No"; - universe_decl = pl; - strength = kind } in + strength = kind; + universe_decl = pl } in push initial_state pstates let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals terminator = @@ -265,9 +186,8 @@ let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals termina proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals; endline_tactic = None; section_vars = None; - mode = find_proof_mode "No"; - universe_decl = pl; - strength = kind } in + strength = kind; + universe_decl = pl } in push initial_state pstates let get_used_variables () = (cur_pstate ()).section_vars @@ -443,8 +363,13 @@ let return_proof ?(allow_partial=false) () = (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate side-effects... This may explain why one need to uniquize side-effects thereafter... *) + let proof_opt c = + match EConstr.to_constr_opt evd c with + | Some p -> p + | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain") + in let proofs = - List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in + List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in proofs, Evd.evar_universe_context evd let close_future_proof ~opaque ~feedback_id proof = @@ -473,7 +398,7 @@ end let freeze ~marshallable = if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") else !pstates -let unfreeze s = pstates := s; update_proof_mode () +let unfreeze s = pstates := s let proof_of_state = function { proof }::_ -> proof | _ -> raise NoCurrentProof let copy_terminators ~src ~tgt = assert(List.length src = List.length tgt); diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index e762f3b7dc..40920f51a3 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -13,7 +13,6 @@ environment. *) type t - val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -139,47 +138,3 @@ val freeze : marshallable:bool -> t val unfreeze : t -> unit val proof_of_state : t -> Proof.t val copy_terminators : src:t -> tgt:t -> t - - -(**********************************************************) -(* Proof Mode API *) -(* The current Proof Mode API is deprecated and a new one *) -(* will be (hopefully) defined in 8.8 *) -(**********************************************************) - -(** Type of proof modes : - - A name - - A function [set] to set it *from standard mode* - - A function [reset] to reset the *standard mode* from it - -*) -type proof_mode_name = string -type proof_mode = { - name : proof_mode_name ; - set : unit -> unit ; - reset : unit -> unit -} - -(** Registers a new proof mode which can then be adressed by name - in [set_default_proof_mode]. - One mode is already registered - the standard mode - named "No", - It corresponds to Coq default setting are they are set when coqtop starts. *) -val register_proof_mode : proof_mode -> unit -(* Can't make this deprecated due to limitations of camlp5 *) -(* [@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] *) - -val proof_mode_opt_name : string list - -val get_default_proof_mode_name : unit -> proof_mode_name -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -(** [set_proof_mode] sets the proof mode to be used after it's called. It is - typically called by the Proof Mode command. *) -val set_proof_mode : proof_mode_name -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -val activate_proof_mode : proof_mode_name -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] - -val disactivate_current_proof_mode : unit -> unit -[@@ocaml.deprecated "the current proof mode API is deprecated, use with care, see PR #459 and #566 "] |