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 53c146bfc..423c95509 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -367,7 +367,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.tabulate meta pac.arity) in let all_args = List.rev_append real_args dummy_args in applistc (mkConstruct cinfo.ci_constr) all_args |