diff options
Diffstat (limited to 'proofs/pfedit.mli')
| -rw-r--r-- | proofs/pfedit.mli | 108 |
1 files changed, 20 insertions, 88 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index ea604e08..65cde3a3 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -1,52 +1,20 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** Global proof state. A quite redundant wrapper on {!Proof_global}. *) -open Loc open Names -open Term +open Constr open Environ open Decl_kinds -(** Several proofs can be opened simultaneously but at most one is - focused at some time. The following functions work by side-effect - on current set of open proofs. In this module, ``proofs'' means an - open proof (something started by vernacular command [Goal], [Lemma] - or [Theorem]), and ``goal'' means a subgoal of the current focused - proof *) - -(** {6 ... } *) -(** [refining ()] tells if there is some proof in progress, even if a not - focused one *) - -val refining : unit -> bool - -(** [check_no_pending_proofs ()] fails if there is still some proof in - progress *) - -val check_no_pending_proofs : unit -> unit - -(** {6 ... } *) -(** [delete_proof name] deletes proof of name [name] or fails if no proof - has this name *) - -val delete_proof : Id.t located -> unit - -(** [delete_current_proof ()] deletes current focused proof or fails if - no proof is focused *) - -val delete_current_proof : unit -> unit - -(** [delete_all_proofs ()] deletes all open proofs if any *) - -val delete_all_proofs : unit -> unit - (** {6 ... } *) (** [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 @@ -55,12 +23,8 @@ val delete_all_proofs : unit -> unit systematically apply at initialization time (e.g. to start the proof of mutually dependent theorems) *) -type lemma_possible_guards = Proof_global.lemma_possible_guards - -type universe_binders = Id.t Loc.located list - val start_proof : - Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> constr -> + Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr -> ?init_tac:unit Proofview.tactic -> Proof_global.proof_terminator -> unit @@ -73,18 +37,13 @@ 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_pftreestate ()] returns the current focused pending proof. - @raise NoCurrentProof if there is no pending proof. *) - -val get_pftreestate : unit -> Proof.proof - (** [get_goal_context n] returns the context of the [n]th subgoal of the current focused proof or raises a [UserError] if there is no focused proof or if there is no more subgoals *) @@ -106,37 +65,10 @@ val get_current_context : unit -> Evd.evar_map * env (** [current_proof_statement] *) val current_proof_statement : - unit -> Id.t * goal_kind * types + unit -> Id.t * goal_kind * EConstr.types (** {6 ... } *) -(** [get_current_proof_name ()] return the name of the current focused - proof or failed if no proof is focused *) - -val get_current_proof_name : unit -> Id.t -(** [get_all_proof_names ()] returns the list of all pending proof names. - The first name is the current proof, the other names may come in - any order. *) - -val get_all_proof_names : unit -> Id.t list - -(** {6 ... } *) -(** [set_end_tac tac] applies tactic [tac] to all subgoal generate - by [solve] *) - -val set_end_tac : Tacexpr.raw_tactic_expr -> unit - -(** {6 ... } *) -(** [set_used_variables l] declares that section variables [l] will be - used in the proof *) -val set_used_variables : - Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list -val get_used_variables : unit -> Context.section_context option - -(** {6 Universe binders } *) -val get_universe_binders : unit -> universe_binders option - -(** {6 ... } *) (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th subgoal of the current focused proof or raises a [UserError] if no proof is focused or if there is no [n]th subgoal. [solve SelectAll @@ -144,7 +76,7 @@ val get_universe_binders : unit -> universe_binders option 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 @@ -165,16 +97,16 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit tactic. *) val build_constant_by_tactic : - Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> - types -> unit Proofview.tactic -> + Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind -> + EConstr.types -> unit Proofview.tactic -> Safe_typing.private_constants Entries.definition_entry * bool * - Evd.evar_universe_context + UState.t -val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> - types -> unit Proofview.tactic -> - constr * bool * Evd.evar_universe_context +val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> + EConstr.types -> unit Proofview.tactic -> + constr * bool * UState.t -val refine_by_tactic : env -> Evd.evar_map -> types -> unit Proofview.tactic -> +val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> constr * Evd.evar_map (** A variant of the above function that handles open terms as well. Caveat: all effects are purged in the returned term at the end, but other @@ -190,4 +122,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr +val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option |