diff options
| author | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-13 17:13:44 +0100 |
| commit | 8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch) | |
| tree | 675b02e411ff2c56a9aff39f4956a055eac254a7 /kernel/opaqueproof.mli | |
| parent | 29a7307ea7cd36408661ba633a235793f11dca84 (diff) | |
| parent | 03e21974a3e971a294533bffb81877dc1bd270b6 (diff) | |
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'kernel/opaqueproof.mli')
| -rw-r--r-- | kernel/opaqueproof.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index a0418a022f..20d76ce238 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -7,7 +7,7 @@ (************************************************************************) open Names -open Term +open Constr open Mod_subst (** This module implements the handling of opaque proof terms. @@ -19,7 +19,7 @@ open Mod_subst When it is [turn_indirect] the data is relocated to an opaque table and the [opaque] is turned into an index. *) -type proofterm = (constr * Univ.universe_context_set) Future.computation +type proofterm = (constr * Univ.ContextSet.t) Future.computation type opaquetab type opaque @@ -36,10 +36,10 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab (** From a [opaque] back to a [constr]. This might use the indirect opaque accessor configured below. *) val force_proof : opaquetab -> opaque -> constr -val force_constraints : opaquetab -> opaque -> Univ.universe_context_set -val get_proof : opaquetab -> opaque -> Term.constr Future.computation +val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t +val get_proof : opaquetab -> opaque -> constr Future.computation val get_constraints : - opaquetab -> opaque -> Univ.universe_context_set Future.computation option + opaquetab -> opaque -> Univ.ContextSet.t Future.computation option val subst_opaque : substitution -> opaque -> opaque val iter_direct_opaque : (constr -> unit) -> opaque -> opaque @@ -63,7 +63,7 @@ val join_opaque : opaquetab -> opaque -> unit val dump : opaquetab -> Constr.t Future.computation array * - Univ.universe_context_set Future.computation array * + Univ.ContextSet.t Future.computation array * cooking_info list array * int Future.UUIDMap.t @@ -75,7 +75,7 @@ val dump : opaquetab -> *) val set_indirect_opaque_accessor : - (DirPath.t -> int -> Term.constr Future.computation) -> unit + (DirPath.t -> int -> constr Future.computation) -> unit val set_indirect_univ_accessor : - (DirPath.t -> int -> Univ.universe_context_set Future.computation option) -> unit + (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit |