aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/cctac.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc/cctac.ml')
-rw-r--r--plugins/cc/cctac.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 423c95509..3b2e42d4e 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -101,7 +101,7 @@ let rec pattern_of_constr env sigma c =
App (f,args)->
let pf = decompose_term env sigma f in
let pargs,lrels = List.split
- (array_map_to_list (pattern_of_constr env sigma) args) in
+ (Array.map_to_list (pattern_of_constr env sigma) args) in
PApp (pf,List.rev pargs),
List.fold_left Intset.union Intset.empty lrels
| Prod (_,a,_b) when not (Termops.dependent (mkRel 1) _b) ->