Merge PR #13180: Respect Print Universes when printing primitive arrays

Reviewed-by: herbelin
coq · Oct 20, 2020 · 1111093 · 1111093
2 parents 48319ad + 5da6b8c
commit 1111093
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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)