From 441bea723c511ed9e18ef005678bd01242b45c49 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 13 Dec 2017 13:57:10 +0100
Subject: 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.
---
 vernac/record.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac')

diff --git a/vernac/record.ml b/vernac/record.ml
index d9dc16d96e..1e464eb8bf 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
-- 
cgit v1.2.3