diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0ce8a8aac4..d5f96e3fd6 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1015,7 +1015,7 @@ let any_any_branch = let rec glob_of_pat env = function | PRef ref -> GRef (loc,ref) | PVar id -> GVar (loc,id) - | PEvar (n,l) -> GEvar (loc,n,Some (array_map_to_list (glob_of_pat env) l)) + | PEvar (n,l) -> GEvar (loc,n,Some (Array.map_to_list (glob_of_pat env) l)) | PRel n -> let id = try match lookup_name_of_rel n env with | Name id -> id @@ -1026,7 +1026,7 @@ let rec glob_of_pat env = function | PMeta None -> GHole (loc,Evar_kinds.InternalHole) | PMeta (Some n) -> GPatVar (loc,(false,n)) | PApp (f,args) -> - GApp (loc,glob_of_pat env f,array_map_to_list (glob_of_pat env) args) + GApp (loc,glob_of_pat env f,Array.map_to_list (glob_of_pat env) args) | PSoApp (n,args) -> GApp (loc,GPatVar (loc,(true,n)), List.map (glob_of_pat env) args) |