diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-09-25 10:49:18 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-09-25 10:49:18 +0200 |
| commit | 43cd1660807b7da915d405d7aa9af8082b5d85f6 (patch) | |
| tree | 6ed698aed58641eee9608a41b310e0bc7517c0b0 /pretyping | |
| parent | f48ada1566daa5245244be3706c1b8c71237c374 (diff) | |
| parent | 6d1b7368267a4da980980efa682cf3fb8f1e8394 (diff) | |
Merge PR #1083: Fixing bug in building _rect scheme for inductive types with let-ins and non-recursively uniform parameters
Diffstat (limited to 'pretyping')
| -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 |