From 5da6b8c6546c2c1823592deb0bc1c64e85de0065 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 12 Oct 2020 15:15:12 +0200
Subject: Respect Print Universes when printing primitive arrays

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

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 167ea3ecdf..7dd8b30bb4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1103,7 +1103,7 @@ let rec extern inctx ?impargs scopes vars r =
   | GFloat f -> extern_float f (snd scopes)
 
   | GArray(u,t,def,ty) ->
-    CArray(u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty)
+    CArray(extern_universes u,Array.map (extern inctx scopes vars) t, extern inctx scopes vars def, extern_typ scopes vars ty)
 
   in insert_entry_coercion coercion (CAst.make ?loc c)
 
-- 
cgit v1.2.3