From 601ce3738253e4bb197900ee6dad271c4e3666d6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 27 Sep 2018 14:23:25 +0200
Subject: Adding universe names to polymorphic entry instances.

---
 interp/modintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/modintern.ml')

diff --git a/interp/modintern.ml b/interp/modintern.ml
index 51e27299e3..93aa271e8b 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -107,7 +107,7 @@ let transl_with_decl env base kind = function
     let c, ectx = interp_constr env sigma c in
     let poly = lookup_polymorphism env base kind fqid in
     begin match UState.check_univ_decl ~poly ectx udecl with
-      | Entries.Polymorphic_const_entry ctx ->
+      | Entries.Polymorphic_const_entry (nas, ctx) ->
         let inst, ctx = Univ.abstract_universes ctx in
         let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
         let c = EConstr.to_constr sigma c in
-- 
cgit v1.2.3