aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml2
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)