diff options
Diffstat (limited to 'plugins/cc')
| -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 73c050bb2..70aaa0c0f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -65,7 +65,7 @@ let rec decompose_term env sigma t= let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in - let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in + let nargs=constructor_nallargs_env env (canon_ind,i_con) in Constructor {ci_constr= ((canon_ind,i_con),u); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} |