diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:27:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:46:52 +0100 |
| commit | 03e21974a3e971a294533bffb81877dc1bd270b6 (patch) | |
| tree | 1b37339378f6bc93288b61f707efb6b08f992dc5 /kernel/opaqueproof.mli | |
| parent | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff) | |
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
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 a0418a022..20d76ce23 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 |