diff options
Diffstat (limited to 'plugins/cc/cctac.ml')
| -rw-r--r-- | plugins/cc/cctac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 20cf9edb8..a5baa00f9 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -365,7 +365,7 @@ let discriminate_tac cstr p gls = let build_term_to_complete uf meta pac = let cinfo = get_constructor_info uf pac.cnode in let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in - let dummy_args = List.rev (List.tabulate meta pac.arity) in + let dummy_args = List.rev (List.init pac.arity meta) in let all_args = List.rev_append real_args dummy_args in applistc (mkConstruct cinfo.ci_constr) all_args |