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 ++--
 test-suite/success/Inductive.v | 17 +++++++++++++++++
 2 files changed, 19 insertions(+), 2 deletions(-)

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
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index f746def5cb..06f807f29a 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -183,3 +183,20 @@ Module PolyNoLowerProp.
   Fail Check Foo True : Prop.
 
 End PolyNoLowerProp.
+
+(* Test building of elimination scheme with noth let-ins and
+   non-recursively uniform parameters *)
+
+Module NonRecLetIn.
+
+  Unset Implicit Arguments.
+
+  Inductive Ind (b:=2) (a:nat) (c:=1) : Type :=
+  | Base : Ind a
+  | Rec : Ind (S a) -> Ind a.
+
+  Check Ind_rect (fun n (b:Ind n) => b = b)
+    (fun n => eq_refl)
+    (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)).
+
+End NonRecLetIn.
-- 
cgit v1.2.3