diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d95554de56..987aa63392 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -772,7 +772,7 @@ let rec adjust_env env = function | NCast (c,_) -> adjust_env env c | NApp _ -> restart_no_binders env | NVar _ | NRef _ | NHole _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NInt _ | NFloat _ + | NRec _ | NSort _ | NInt _ | NFloat _ | NArray _ | NList _ | NBinderList _ -> env (* to be safe, but restart should be ok *) let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = @@ -2204,6 +2204,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | CCast (c1, c2) -> DAst.make ?loc @@ GCast (intern env c1, map_cast_type (intern_type (slide_binders env)) c2) + | CArray(u,t,def,ty) -> + DAst.make ?loc @@ GArray(u, Array.map (intern env) t, intern env def, intern env ty) ) and intern_type env = intern (set_type_scope env) |