diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/goal.mli | 2 | ||||
-rw-r--r-- | proofs/pfedit.ml | 2 | ||||
-rw-r--r-- | proofs/pfedit.mli | 6 | ||||
-rw-r--r-- | proofs/proof.ml | 4 | ||||
-rw-r--r-- | proofs/proof.mli | 60 | ||||
-rw-r--r-- | proofs/proof_bullet.ml | 8 | ||||
-rw-r--r-- | proofs/proof_bullet.mli | 10 | ||||
-rw-r--r-- | proofs/proof_global.ml | 15 | ||||
-rw-r--r-- | proofs/proof_global.mli | 24 |
9 files changed, 67 insertions, 64 deletions
diff --git a/proofs/goal.mli b/proofs/goal.mli index ad968cdfb..37dd9d3c0 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -58,7 +58,7 @@ module V82 : sig (* Principal part of the progress tactical *) val progress : goal list Evd.sigma -> goal Evd.sigma -> bool - + (* Principal part of tclNOTSAMEGOAL *) val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c526ae000..31a73db04 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -140,7 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo let status = by tac in let _,(const,univs,_) = cook_proof () in Proof_global.discard_current (); - const, status, fst univs + const, status, univs with reraise -> let reraise = CErrors.push reraise in Proof_global.discard_current (); diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index d676a0874..5a317a956 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -35,11 +35,11 @@ val start_proof : val cook_this_proof : Proof_global.proof_object -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) val cook_proof : unit -> (Id.t * - (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind)) + (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind)) (** {6 ... } *) (** [get_goal_context n] returns the context of the [n]th subgoal of @@ -74,7 +74,7 @@ val current_proof_statement : val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> - Proof.proof -> Proof.proof*bool + Proof.t -> Proof.t * bool (** [by tac] applies tactic [tac] to the 1st subgoal of the current focused proof or raises a UserError if there is no focused proof or diff --git a/proofs/proof.ml b/proofs/proof.ml index 413b5fdd7..04e707cd6 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -98,7 +98,7 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k) (* Subpart of the type of proofs. It contains the parts of the proof which are under control of the undo mechanism *) -type proof = { +type t = { (* Current focused proofview *) proofview: Proofview.proofview; (* Entry for the proofview *) @@ -115,6 +115,8 @@ type proof = { initial_euctx : UState.t } +type proof = t + (*** General proof functions ***) let proof p = diff --git a/proofs/proof.mli b/proofs/proof.mli index 83777fc96..0b5e771ef 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -30,7 +30,9 @@ *) (* Type of a proof. *) -type proof +type t +type proof = t +[@@ocaml.deprecated "please use [Proof.t]"] (* Returns a stylised view of a proof for use by, for instance, ide-s. *) @@ -42,7 +44,7 @@ type proof shelf (the list of goals on the shelf), a representation of the given up goals (the list of the given up goals) and the underlying evar_map *) -val proof : proof -> +val proof : t -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Goal.goal list @@ -61,26 +63,26 @@ type 'a pre_goals = { (** List of the goals that have been given up *) } -val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) +val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) (*** General proof functions ***) -val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof -val dependent_start : Proofview.telescope -> proof -val initial_goals : proof -> (EConstr.constr * EConstr.types) list -val initial_euctx : proof -> UState.t +val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t +val dependent_start : Proofview.telescope -> t +val initial_goals : t -> (EConstr.constr * EConstr.types) list +val initial_euctx : t -> UState.t (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) -val is_done : proof -> bool +val is_done : t -> bool (* Like is_done, but this time it really means done (i.e. nothing left to do) *) -val is_complete : proof -> bool +val is_complete : t -> bool (* Returns the list of partial proofs to initial goals. *) -val partial_proof : proof -> EConstr.constr list +val partial_proof : t -> EConstr.constr list -val compact : proof -> proof +val compact : t -> t (* Returns the proofs (with their type) of the initial goals. Raises [UnfinishedProof] is some goals remain to be considered. @@ -91,7 +93,7 @@ exception UnfinishedProof exception HasShelvedGoals exception HasGivenUpGoals exception HasUnresolvedEvar -val return : proof -> Evd.evar_map +val return : t -> Evd.evar_map (*** Focusing actions ***) @@ -131,7 +133,7 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition (* focus command (focuses on the [i]th subgoal) *) (* spiwack: there could also, easily be a focus-on-a-range tactic, is there a need for it? *) -val focus : 'a focus_condition -> 'a -> int -> proof -> proof +val focus : 'a focus_condition -> 'a -> int -> t -> t exception FullyUnfocused exception CannotUnfocusThisWay @@ -147,59 +149,59 @@ exception NoSuchGoals of int * int Raises [FullyUnfocused] if the proof is not focused. Raises [CannotUnfocusThisWay] if the proof the unfocusing condition is not met. *) -val unfocus : 'a focus_kind -> proof -> unit -> proof +val unfocus : 'a focus_kind -> t -> unit -> t (* [unfocused p] returns [true] when [p] is fully unfocused. *) -val unfocused : proof -> bool +val unfocused : t -> bool (* [get_at_focus k] gets the information stored at the closest focus point of kind [k]. Raises [NoSuchFocus] if there is no focus point of kind [k]. *) exception NoSuchFocus -val get_at_focus : 'a focus_kind -> proof -> 'a +val get_at_focus : 'a focus_kind -> t -> 'a (* [is_last_focus k] check if the most recent focus is of kind [k] *) -val is_last_focus : 'a focus_kind -> proof -> bool +val is_last_focus : 'a focus_kind -> t -> bool (* returns [true] if there is no goal under focus. *) -val no_focused_goal : proof -> bool +val no_focused_goal : t -> bool (*** Tactics ***) (* the returned boolean signal whether an unsafe tactic has been used. In which case it is [false]. *) val run_tactic : Environ.env -> - unit Proofview.tactic -> proof -> proof*(bool*Proofview_monad.Info.tree) + unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) -val maximal_unfocus : 'a focus_kind -> proof -> proof +val maximal_unfocus : 'a focus_kind -> t -> t (*** Commands ***) -val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a +val in_proof : t -> (Evd.evar_map -> 'a) -> 'a (* Remove all the goals from the shelf and adds them at the end of the focused goals. *) -val unshelve : proof -> proof +val unshelve : t -> t -val pr_proof : proof -> Pp.t +val pr_proof : t -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig - val subgoals : proof -> Goal.goal list Evd.sigma + val subgoals : t -> Goal.goal list Evd.sigma [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] (* All the subgoals of the proof, including those which are not focused. *) - val background_subgoals : proof -> Goal.goal list Evd.sigma + val background_subgoals : t -> Goal.goal list Evd.sigma - val top_goal : proof -> Goal.goal Evd.sigma + val top_goal : t -> Goal.goal Evd.sigma (* returns the existential variable used to start the proof *) - val top_evars : proof -> Evar.t list + val top_evars : t -> Evar.t list (* Turns the unresolved evars into goals. Raises [UnfinishedProof] if there are still unsolved goals. *) - val grab_evars : proof -> proof + val grab_evars : t -> t (* Implements the Existential command *) - val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> proof + val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t end diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 4f575ab4b..214916331 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -25,8 +25,8 @@ let pr_bullet b = type behavior = { name : string; - put : proof -> t -> proof; - suggest: proof -> Pp.t + put : Proof.t -> t -> Proof.t; + suggest: Proof.t -> Pp.t } let behaviors = Hashtbl.create 4 @@ -110,7 +110,7 @@ module Strict = struct let push (b:t) pr = focus bullet_cond (b::get_bullets pr) 1 pr - let suggest_bullet (prf : proof): suggestion = + let suggest_bullet (prf : Proof.t): suggestion = if is_done prf then ProofFinished else if not (no_focused_goal prf) then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *) @@ -137,7 +137,7 @@ module Strict = struct in loop prf - let rec pop_until (prf : proof) bul : proof = + let rec pop_until (prf : Proof.t) bul : Proof.t = let prf', b = pop prf in if bullet_eq bul b then prf' else pop_until prf' bul diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index 9e924fec9..09fcabf50 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -12,8 +12,6 @@ (* *) (**********************************************************) -open Proof - type t = Vernacexpr.bullet (** A [behavior] is the data of a put function which @@ -22,8 +20,8 @@ type t = Vernacexpr.bullet with a name to identify the behavior. *) type behavior = { name : string; - put : proof -> t -> proof; - suggest: proof -> Pp.t + put : Proof.t -> t -> Proof.t; + suggest: Proof.t -> Pp.t } (** A registered behavior can then be accessed in Coq @@ -39,8 +37,8 @@ val register_behavior : behavior -> unit (** Handles focusing/defocusing with bullets: *) -val put : proof -> t -> proof -val suggest : proof -> Pp.t +val put : Proof.t -> t -> Proof.t +val suggest : Proof.t -> Pp.t (**********************************************************) (* *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index aa5621770..535ef2013 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -68,17 +68,16 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = - | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes + | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -90,12 +89,15 @@ type pstate = { terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; section_vars : Context.Named.t option; - proof : Proof.proof; + proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; universe_decl: Univdecls.universe_decl; } +type t = pstate list +type state = t + let make_terminator f = f let apply_terminator f = f @@ -330,7 +332,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let fpl, univs = Future.split2 fpl in let universes = if poly || now then Future.force univs else initial_euctx in - let binders = if poly then Some (UState.universe_binders universes) else None in (* Because of dependent subgoals at the beginning of proofs, we could have existential variables in the initial types of goals, we need to normalise them for the kernel. *) @@ -406,7 +407,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now in let entries = Future.map2 entry_fn fpl initial_goals in { id = pid; entries = entries; persistence = strength; - universes = (universes, binders) }, + universes }, fun pr_ending -> CEphemeron.get terminator pr_ending let return_proof ?(allow_partial=false) () = @@ -467,8 +468,6 @@ module V82 = struct pid, (goals, strength) end -type state = pstate list - let freeze ~marshallable = match marshallable with | `Yes -> diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index eed62f912..27e99f218 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -10,6 +10,10 @@ toplevel. In particular it defines the global proof environment. *) +type t +type state = t +[@@ocaml.deprecated "please use [Proof_global.t]"] + val there_are_pending_proofs : unit -> bool val check_no_pending_proof : unit -> unit @@ -21,7 +25,7 @@ val discard_current : unit -> unit val discard_all : unit -> unit exception NoCurrentProof -val give_me_the_proof : unit -> Proof.proof +val give_me_the_proof : unit -> Proof.t (** @raise NoCurrentProof when outside proof mode. *) val compact_the_proof : unit -> unit @@ -33,18 +37,17 @@ val compact_the_proof : unit -> unit (i.e. an proof ending command) and registers the appropriate values. *) type lemma_possible_guards = int list list -type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - proof_universes + UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -107,9 +110,9 @@ val get_open_goals : unit -> int no current proof. The return boolean is set to [false] if an unsafe tactic has been used. *) val with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof*'a) -> 'a + (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a val simple_with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit + (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Genarg.glob_generic_argument -> unit @@ -129,11 +132,10 @@ module V82 : sig Decl_kinds.goal_kind) end -type state -val freeze : marshallable:[`Yes | `No | `Shallow] -> state -val unfreeze : state -> unit -val proof_of_state : state -> Proof.proof -val copy_terminators : src:state -> tgt:state -> state +val freeze : marshallable:[`Yes | `No | `Shallow] -> t +val unfreeze : t -> unit +val proof_of_state : t -> Proof.t +val copy_terminators : src:t -> tgt:t -> t (**********************************************************) |