diff options
| author | Pierre-Marie Pédrot | 2019-06-10 12:27:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-17 15:20:03 +0200 |
| commit | a69bb15b1d76b71628b61bc42eb8d79c098074a8 (patch) | |
| tree | 942ea34a92f2eebf7a442288546233b25065856a /kernel/opaqueproof.mli | |
| parent | 5316d205993bb3fe3f69e8984fe53d4d50aa8d2a (diff) | |
Merge universe quantification and delayed constraints in opaque proofs.
This enforces more invariants statically.
Diffstat (limited to 'kernel/opaqueproof.mli')
| -rw-r--r-- | kernel/opaqueproof.mli | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 20c862c651..8b844e0812 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -23,7 +23,8 @@ open Mod_subst type 'a delayed_universes = | PrivateMonomorphic of 'a -| PrivatePolymorphic of Univ.ContextSet.t +| PrivatePolymorphic of int * Univ.ContextSet.t + (** Number of surrounding bound universes + local constraints *) type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation type opaquetab @@ -32,7 +33,7 @@ type opaque val empty_opaquetab : opaquetab (** From a [proofterm] to some [opaque]. *) -val create : univs:int -> proofterm -> opaque +val create : proofterm -> opaque (** Turn a direct [opaque] into an indirect one. It is your responsibility to hashcons the inner term beforehand. The integer is an hint of the maximum id @@ -46,11 +47,11 @@ type cooking_info = { modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } -type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option +type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option type indirect_accessor = { access_proof : DirPath.t -> int -> opaque_proofterm; - access_discharge : cooking_info list -> int -> + access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); } (** When stored indirectly, opaque terms are indexed by their library |