diff options
Diffstat (limited to 'kernel/opaqueproof.mli')
| -rw-r--r-- | kernel/opaqueproof.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 4646206e55..46b0500507 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -37,7 +37,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab type indirect_accessor = { access_proof : DirPath.t -> int -> constr option; - access_constraints : DirPath.t -> int -> Univ.ContextSet.t option; } (** When stored indirectly, opaque terms are indexed by their library dirpath and an integer index. The two functions above activate @@ -70,6 +69,5 @@ val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit val dump : ?except:Future.UUIDSet.t -> opaquetab -> Constr.t option array * - Univ.ContextSet.t option array * cooking_info list array * int Future.UUIDMap.t |