diff options
| author | Pierre-Marie Pédrot | 2019-05-16 00:02:54 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-20 14:10:58 +0200 |
| commit | 27468ae02bbbf018743d53a9db49efa34b6d6a3e (patch) | |
| tree | e8fa5ad95ba323d76af06d24e9d804a0dae94844 /kernel/opaqueproof.mli | |
| parent | 801aed67a90ec49c15a4469e1905aa2835fabe19 (diff) | |
Ensure statically that declarations built by Term_typing are direct.
This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
Diffstat (limited to 'kernel/opaqueproof.mli')
| -rw-r--r-- | kernel/opaqueproof.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index d47c0bbb3c..8b6e8a1c8f 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -39,6 +39,7 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab indirect opaque accessor configured below. *) val force_proof : opaquetab -> opaque -> constr val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t +val force_direct : opaque -> (constr * Univ.ContextSet.t) val get_constraints : opaquetab -> opaque -> Univ.ContextSet.t Future.computation option |