diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-28 19:41:17 +0100 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-28 19:43:26 +0100 |
commit | 90fef3ffd236f2ed5575b0d11a47185185abc75b (patch) | |
tree | 2768466af2fc67d61a9e9e94e89fb632d54f3c72 /proofs/proof_global.mli | |
parent | 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 (diff) |
Univs: correctly register universe binders for lemmas.
Diffstat (limited to 'proofs/proof_global.mli')
-rw-r--r-- | proofs/proof_global.mli | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index a22545080..ea7fc7cfa 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -55,18 +55,18 @@ 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 = Evd.evar_universe_context +type proof_universes = Evd.evar_universe_context * Universes.universe_binders option +type universe_binders = Names.Id.t Loc.located list type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; universes: proof_universes; - (* constraints : Univ.constraints; *) - (** guards : lemma_possible_guards; *) } 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 * + proof_universes | Proved of Vernacexpr.opacity_flag * (Vernacexpr.lident * Decl_kinds.theorem_kind option) option * proof_object @@ -80,14 +80,15 @@ type closed_proof = proof_object * proof_terminator closing commands and the xml plugin); [terminator] is used at the end of the proof to close the proof. *) val start_proof : - Evd.evar_map -> Names.Id.t -> Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> + Evd.evar_map -> Names.Id.t -> ?pl:universe_binders -> + Decl_kinds.goal_kind -> (Environ.env * Term.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof : - Names.Id.t -> Decl_kinds.goal_kind -> Proofview.telescope -> - proof_terminator -> unit + Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind -> + Proofview.telescope -> proof_terminator -> unit (** Update the proofs global environment after a side-effecting command (e.g. a sublemma definition) has been run inside it. Assumes @@ -140,6 +141,8 @@ val set_used_variables : Names.Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list val get_used_variables : unit -> Context.section_context option +val get_universe_binders : unit -> universe_binders option + (**********************************************************) (* *) (* Proof modes *) |