diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-13 13:57:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-30 19:19:03 +0100 |
| commit | 441bea723c511ed9e18ef005678bd01242b45c49 (patch) | |
| tree | bbe502a899b3b1fa16cb91a7372a2bf2c601ec83 /kernel/opaqueproof.mli | |
| parent | 6e49d0bee79cd68495955deb115b495fb01f01fd (diff) | |
Returning instance instead of substitution in universe context abstraction.
This datatype enforces stronger invariants, e.g. that we only have in the
substitution codomain a connex interval of variables from 0 to n - 1.
Diffstat (limited to 'kernel/opaqueproof.mli')
| -rw-r--r-- | kernel/opaqueproof.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 20d76ce23..c8339e6eb 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t } + abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t } (* The type has two caveats: 1) cook_constr is defined after |