diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 3 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
2 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index c40a24e3b7..e1576b9713 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -234,7 +234,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function let acc = Option.fold_left (f v') acc rtntypopt in List.fold_left fold_pattern acc pl | GLetTuple (nal,rtntyp,b,c) -> - f v (f v (fold_return_type_with_binders f g v acc rtntyp) b) c + f (List.fold_right (Name.fold_right g) nal v) + (f v (fold_return_type_with_binders f g v acc rtntyp) b) c | GIf (c,rtntyp,b1,b2) -> f v (f v (f v (fold_return_type_with_binders f g v acc rtntyp) c) b1) b2 | GRec (_,idl,bll,tyl,bv) -> diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 88ca9b5ca8..b31ee03d8c 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -397,8 +397,8 @@ let get_arity env ((ind,u),params) = mib.mind_params_ctxt else begin assert (Int.equal nparams mib.mind_nparams_rec); - let nnonrecparamdecls = List.length mib.mind_params_ctxt - mib.mind_nparams_rec in - snd (List.chop nnonrecparamdecls mib.mind_params_ctxt) + let nnonrecparamdecls = mib.mind_nparams - mib.mind_nparams_rec in + snd (Termops.context_chop nnonrecparamdecls mib.mind_params_ctxt) end in let parsign = Vars.subst_instance_context u parsign in let arproperlength = List.length mip.mind_arity_ctxt - List.length parsign in |