diff options
| author | Maxime Dénès | 2018-06-01 13:49:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-06-01 13:49:34 +0200 |
| commit | 3a36761a27487e8917e1b59b59abacc2a7e65b95 (patch) | |
| tree | f1cd9d412c40933ff3e87f720dbd8e7cba7f9bbf /proofs/proof_global.mli | |
| parent | ac0bb15616550d00f5e6e7d6239e3b7ff2632975 (diff) | |
| parent | 63b530234e0b19323a50c52434a7439518565c81 (diff) | |
Merge PR #7570: [api] Move `Constrexpr` to the `interp` module.
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index de4cec488a..0141cacb9e 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -71,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit evar map [sigma] (which can typically contain universe constraints), and with universe bindings pl. *) val start_proof : - Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl -> + Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list -> proof_terminator -> unit (** Like [start_proof] except that there may be dependencies between initial goals. *) val start_dependent_proof : - Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> + Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit (** Update the proofs global environment after a side-effecting command @@ -130,7 +130,7 @@ val set_used_variables : val get_used_variables : unit -> Context.Named.t option (** Get the universe declaration associated to the current proof. *) -val get_universe_decl : unit -> Univdecls.universe_decl +val get_universe_decl : unit -> UState.universe_decl module V82 : sig val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list * |