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 /library/lib.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 'library/lib.mli')
| -rw-r--r-- | library/lib.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/lib.mli b/library/lib.mli index 2f4d0d56f..cf75d5f8c 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -156,8 +156,8 @@ type variable_context = variable_info list type abstr_info = private { abstr_ctx : variable_context; (** Section variables of this prefix *) - abstr_subst : Univ.universe_level_subst; - (** Abstract substitution: named universes are mapped to De Bruijn indices *) + abstr_subst : Univ.Instance.t; + (** Actual names of the abstracted variables *) abstr_uctx : Univ.AUContext.t; (** Universe quantification, same length as the substitution *) } |