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 /vernac/record.ml | |
| 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 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index d9dc16d96..1e464eb8b 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -531,6 +531,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari match univs with | Polymorphic_const_entry univs -> let usubst, auctx = Univ.abstract_universes univs in + let usubst = Univ.make_instance_subst usubst in let map c = Vars.subst_univs_level_constr usubst c in let fields = Context.Rel.map map fields in let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in |