diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:05:53 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-11-29 19:13:30 +0100 |
commit | e98d3c3793f26265a49f63a6e78d704f88341df9 (patch) | |
tree | c0328afc0034f3262dca2ca067531ee19bbb0ee0 /proofs/proof_global.mli | |
parent | 103ec7205d9038f1f3821f9287e3bb0907a1e3ec (diff) | |
parent | 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 (diff) |
Merge branch 'v8.5'
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 3fbcefd0a..5f1158950 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 @@ -83,14 +83,15 @@ val apply_terminator : proof_terminator -> proof_ending -> unit 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 @@ -143,6 +144,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 *) |