Merge PR #1083: Fixing bug in building _rect scheme for inductive types with let-ins and non-recursively uniform parameters

2 files changed, 19 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
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index f746def5c..06f807f29 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.