diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 20 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 14 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 72 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 5 |
4 files changed, 49 insertions, 62 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 83eb47bb9..7d225a470 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -29,23 +29,23 @@ let delete_all_proofs = Proof_global.discard_all let set_undo _ = () let get_undo _ = None -let start_proof (id : Id.t) str hyps c ?init_tac hook terminator = +let start_proof (id : Id.t) str hyps c ?init_tac terminator = let goals = [ (Global.env_of_context hyps , c) ] in - Proof_global.start_proof id str goals hook terminator; + Proof_global.start_proof id str goals terminator; let env = Global.env () in ignore (Proof_global.with_current_proof (fun _ p -> match init_tac with | None -> p,true | Some tac -> Proof.run_tactic env tac p)) -let cook_this_proof hook p = +let cook_this_proof p = match p with - | { Proof_global.id;entries=[constr];persistence;hook } -> - (id,(constr,persistence,hook)) + | { Proof_global.id;entries=[constr];persistence } -> + (id,(constr,persistence)) | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") -let cook_proof hook = - cook_this_proof hook (fst (Proof_global.close_proof (fun x -> x))) +let cook_proof () = + cook_this_proof (fst (Proof_global.close_proof (fun x -> x))) let get_pftreestate () = Proof_global.give_me_the_proof () @@ -88,7 +88,7 @@ let get_current_goal_context () = let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with - | (id,([concl],strength,hook)) -> id,strength,concl,hook + | (id,([concl],strength)) -> id,strength,concl | _ -> Errors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") let solve ?with_end_tac gi tac pr = @@ -123,10 +123,10 @@ open Decl_kinds let next = let n = ref 0 in fun () -> incr n; !n let build_constant_by_tactic id sign ?(goal_kind = Global,Proof Theorem) typ tac = - start_proof id goal_kind sign typ (fun _ _ -> ()) (fun _ -> ()); + start_proof id goal_kind sign typ (fun _ -> ()); try let status = by tac in - let _,(const,_,_) = cook_proof (fun _ -> ()) in + let _,(const,_) = cook_proof () in delete_current_proof (); const, status with reraise -> diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 9762d415f..c3d0c9053 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -62,7 +62,7 @@ type lemma_possible_guards = Proof_global.lemma_possible_guards val start_proof : Id.t -> goal_kind -> named_context_val -> constr -> ?init_tac:unit Proofview.tactic -> - unit declaration_hook -> Proof_global.proof_terminator -> unit + Proof_global.proof_terminator -> unit (** {6 ... } *) (** [cook_proof opacity] turns the current proof (assumed completed) into @@ -70,16 +70,14 @@ val start_proof : it fails if there is no current proof of if it is not completed; it also tells if the guardness condition has to be inferred. *) -val cook_this_proof : (Proof.proof -> unit) -> +val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Entries.definition_entry * goal_kind * - unit declaration_hook Ephemeron.key)) + (Entries.definition_entry * goal_kind)) -val cook_proof : (Proof.proof -> unit) -> +val cook_proof : unit -> (Id.t * - (Entries.definition_entry * goal_kind * - unit declaration_hook Ephemeron.key)) + (Entries.definition_entry * goal_kind)) (** {6 ... } *) (** [get_pftreestate ()] returns the current focused pending proof. @@ -100,7 +98,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env (** [current_proof_statement] *) val current_proof_statement : - unit -> Id.t * goal_kind * types * unit declaration_hook Ephemeron.key + unit -> Id.t * goal_kind * types (** {6 ... } *) (** [get_current_proof_name ()] return the name of the current focused diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 2534a1ec7..2f002e941 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -69,7 +69,6 @@ type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - hook : unit Tacexpr.declaration_hook Ephemeron.key } type proof_ending = Vernacexpr.proof_end * proof_object @@ -84,7 +83,6 @@ type pstate = { section_vars : Context.section_context option; proof : Proof.proof; strength : Decl_kinds.goal_kind; - pr_hook : unit Tacexpr.declaration_hook Ephemeron.key; mode : proof_mode Ephemeron.key; } @@ -239,16 +237,13 @@ let _ = Errors.register_handler begin function | _ -> raise Errors.Unhandled end -(* [start_proof s str env t hook tac] starts a proof of name [s] and - conclusion [t]; [hook] is optionally a function to be applied at - proof end (e.g. to declare the built constructions as a coercion - or a setoid morphism); init_tac is possibly a tactic to - systematically apply at initialization time (e.g. to start the - proof of mutually dependent theorems). - It raises exception [ProofInProgress] if there is a proof being - currently edited. *) +(* [start_proof id str goals terminator] starts a proof of name [id] + with goals [goals] (a list of pairs of environment and + conclusion); at the end of the proof [terminator] is called to + close the proof. It raises exception [ProofInProgress] if there + is a proof being currently edited. *) -let start_proof id str goals hook terminator = +let start_proof id str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; @@ -256,11 +251,10 @@ let start_proof id str goals hook terminator = endline_tactic = None; section_vars = None; strength = str; - pr_hook = Ephemeron.create hook; mode = find_proof_mode "No" } in push initial_state pstates -let start_dependent_proof id str goals hook terminator = +let start_dependent_proof id str goals terminator = let initial_state = { pid = id; terminator = Ephemeron.create terminator; @@ -268,7 +262,6 @@ let start_dependent_proof id str goals hook terminator = endline_tactic = None; section_vars = None; strength = str; - pr_hook = Ephemeron.create hook; mode = find_proof_mode "No" } in push initial_state pstates @@ -288,46 +281,45 @@ let set_used_variables l = let get_open_goals () = let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in List.length gl + - List.fold_left (+) 0 + List.fold_left (+) 0 (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) + - List.length shelf + List.length shelf let close_proof ~now fpl = - let { pid;section_vars;strength;pr_hook;proof;terminator } = + let { pid;section_vars;strength;proof;terminator } = cur_pstate () in let initial_goals = Proof.initial_goals proof in let entries = Future.map2 (fun p (c, t) -> { Entries. - const_entry_body = p; - const_entry_secctx = section_vars; - const_entry_type = Some t; - const_entry_inline_code = false; - const_entry_opaque = true }) fpl initial_goals in + const_entry_body = p; + const_entry_secctx = section_vars; + const_entry_type = Some t; + const_entry_inline_code = false; + const_entry_opaque = true }) fpl initial_goals in if now then List.iter (fun x -> ignore(Future.join x.Entries.const_entry_body)) entries; { id = pid ; entries = entries ; - persistence = strength ; - hook = pr_hook } , terminator + persistence = strength } , terminator let return_proof () = let { proof } = cur_pstate () in let initial_goals = Proof.initial_goals proof in let evd = - try Proof.return proof with - | Proof.UnfinishedProof -> - raise (Errors.UserError("last tactic before Qed", - str"Attempt to save an incomplete proof")) - | Proof.HasShelvedGoals -> - raise (Errors.UserError("last tactic before Qed", - str"Attempt to save a proof with shelved goals")) - | Proof.HasGivenUpGoals -> - raise (Errors.UserError("last tactic before Qed", - str"Attempt to save a proof with given up goals")) - | Proof.HasUnresolvedEvar -> - raise (Errors.UserError("last tactic before Qed", - str"Attempt to save a proof with existential " ++ - str"variables still non-instantiated")) + try Proof.return proof with + | Proof.UnfinishedProof -> + raise (Errors.UserError("last tactic before Qed", + str"Attempt to save an incomplete proof")) + | Proof.HasShelvedGoals -> + raise (Errors.UserError("last tactic before Qed", + str"Attempt to save a proof with shelved goals")) + | Proof.HasGivenUpGoals -> + raise (Errors.UserError("last tactic before Qed", + str"Attempt to save a proof with given up goals")) + | Proof.HasUnresolvedEvar -> + raise (Errors.UserError("last tactic before Qed", + str"Attempt to save a proof with existential " ++ + str"variables still non-instantiated")) in let eff = Evd.eval_side_effects evd in (** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate @@ -483,8 +475,8 @@ let _ = module V82 = struct let get_current_initial_conclusions () = - let { pid; strength; pr_hook; proof } = cur_pstate () in - pid, (List.map snd (Proof.initial_goals proof), strength, pr_hook) + let { pid; strength; proof } = cur_pstate () in + pid, (List.map snd (Proof.initial_goals proof), strength) end type state = pstate list diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 71d03438b..ed7668d57 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -57,7 +57,6 @@ type proof_object = { id : Names.Id.t; entries : Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - hook : unit Tacexpr.declaration_hook Ephemeron.key } type proof_ending = Vernacexpr.proof_end * proof_object @@ -73,7 +72,6 @@ type closed_proof = proof_object*proof_terminator Ephemeron.key val start_proof : Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> - unit Tacexpr.declaration_hook -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between @@ -81,7 +79,6 @@ val start_proof : Names.Id.t -> val start_dependent_proof : Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope -> - unit Tacexpr.declaration_hook -> proof_terminator -> unit @@ -177,7 +174,7 @@ val get_default_goal_selector : unit -> Vernacexpr.goal_selector module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * - Decl_kinds.goal_kind * unit Tacexpr.declaration_hook Ephemeron.key) + Decl_kinds.goal_kind) end type state |