From ea083ac106f048e64c1b57ddd37ac717236b8ecd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 14 Feb 2015 12:54:36 +0100
Subject: Univs: When computing the level of an inductive including indices,
 lets do not contribute. Fixes bug #3808.

---
 kernel/indtypes.ml            | 10 ++++++----
 test-suite/bugs/closed/3808.v |  2 ++
 2 files changed, 8 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/3808.v

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index ea575e1e0d..799471c68a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -164,10 +164,12 @@ let infer_constructor_packet env_ar_par ctx params lc =
 (* If indices matter *)
 let cumulate_arity_large_levels env sign =
   fst (List.fold_right
-    (fun (_,_,t as d) (lev,env) ->
-      let tj = infer_type env t in
-      let u = univ_of_sort tj.utj_type in
-	(Universe.sup u lev, push_rel d env))
+    (fun (_,b,t as d) (lev,env) ->
+      if Option.is_empty b then
+	let tj = infer_type env t in
+	let u = univ_of_sort tj.utj_type in
+	  (Universe.sup u lev, push_rel d env)
+      else lev, push_rel d env)
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
diff --git a/test-suite/bugs/closed/3808.v b/test-suite/bugs/closed/3808.v
new file mode 100644
index 0000000000..6e19ddf8dc
--- /dev/null
+++ b/test-suite/bugs/closed/3808.v
@@ -0,0 +1,2 @@
+Inductive Foo : (let enforce := (fun x => x) : Type@{j} -> Type@{i} in Type@{i})
+  := foo : Foo.
\ No newline at end of file
-- 
cgit v1.2.3