diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-23 13:39:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-23 13:53:28 +0200 |
| commit | 6d1b7368267a4da980980efa682cf3fb8f1e8394 (patch) | |
| tree | 30f6a854282e956adcc192bab33650a3fdf66502 /pretyping/inductiveops.ml | |
| parent | 06a723190858da8ed3f30736f22398aa7822c959 (diff) | |
Fixing _rect bug for inductive types with let-ins and non-rec uniform params.
The bug was caused by an inconsistency in different part of the code
for deciding where cutting the context in between recursively uniform
parameters and non-recursively uniform ones when let-ins were in the
middle. We fix it by using uniformly "context_chop".
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 88ca9b5ca..b31ee03d8 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 |