diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/cc/cctac.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/glob_termops.ml | 2 |
4 files changed, 5 insertions, 5 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} diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index cce6aff28..618717cde 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -793,7 +793,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args = and extract_case env mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) - let ni = mis_constr_nargs_env env ip in + let ni = constructors_nrealargs_env env ip in let br_size = Array.length br in assert (Int.equal (Array.length ni) br_size); if Int.equal br_size 0 then begin diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 41970fce8..40abdb68b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -304,7 +304,7 @@ let build_constructors_of_type ind' argl = Impargs.implicits_of_global constructref in let cst_narg = - Inductiveops.mis_constructor_nargs_env + Inductiveops.constructor_nallargs_env (Global.env ()) construct in @@ -388,7 +388,7 @@ let rec pattern_to_term_and_type env typ = function mkGVar id | PatCstr(loc,constr,patternl,_) -> let cst_narg = - Inductiveops.mis_constructor_nargs_env + Inductiveops.constructor_nallargs_env (Global.env ()) constr in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 5efaf7954..4cdea414e 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -427,7 +427,7 @@ let rec pattern_to_term = function mkGVar id | PatCstr(loc,constr,patternl,_) -> let cst_narg = - Inductiveops.mis_constructor_nargs_env + Inductiveops.constructor_nallargs_env (Global.env ()) constr in |