diff options
| author | ppedrot | 2012-09-14 19:13:19 +0000 |
|---|---|---|
| committer | ppedrot | 2012-09-14 19:13:19 +0000 |
| commit | 8cc623262c625bda20e97c75f9ba083ae8e7760d (patch) | |
| tree | 3e7ef244636612606a574a21e4f8acaab828d517 /interp/constrextern.ml | |
| parent | 6eaff635db797d1f9225b22196832c1bb76c0d94 (diff) | |
As r15801: putting everything from Util.array_* to CArray.*.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
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) |