diff options
| author | Gaëtan Gilbert | 2020-10-12 15:15:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-12 15:15:12 +0200 |
| commit | 5da6b8c6546c2c1823592deb0bc1c64e85de0065 (patch) | |
| tree | 8a42a111c5a8b4692b81dca25cecb65e9e964f82 /interp/constrextern.ml | |
| parent | a78b394d372f259107017cdb129be3fe53a15894 (diff) | |
Respect Print Universes when printing primitive arrays
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |