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".
---
 test-suite/success/Inductive.v | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'test-suite')

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