From 6d1b7368267a4da980980efa682cf3fb8f1e8394 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 23 Sep 2017 13:39:48 +0200
Subject: 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".
---
 pretyping/inductiveops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3