diff options
| author | coqbot-app[bot] | 2020-10-20 09:24:07 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-20 09:24:07 +0000 |
| commit | 11110938f4f3b3a570a2047b2f5e060412989e31 (patch) | |
| tree | 0d3b0abe727ae5e53c978fc19c8d7844a01046a5 /interp | |
| parent | 48319ad16a7bff94c3bcfabb37181daa55b568c4 (diff) | |
| parent | 5da6b8c6546c2c1823592deb0bc1c64e85de0065 (diff) | |
Merge PR #13180: Respect Print Universes when printing primitive arrays
Reviewed-by: herbelin
Diffstat (limited to 'interp')
| -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 e5a60769e8..7bf1c58148 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) |