From c2fa953889cf7bcef9c369d175e156855ac0be2e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 10 Sep 2014 12:54:08 +0200
Subject: Fix categorization of recursive inductives.

---
 toplevel/command.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9b650f859a..115c245f38 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -587,6 +587,7 @@ let is_recursive mie =
     | Prod (_,arg,rest) ->
         Termops.dependent (mkRel lift) arg ||
         is_recursive_constructor (lift+1) rest
+    | LetIn (na,b,t,rest) -> is_recursive_constructor (lift+1) rest
     | _ -> false
   in
   match mie.mind_entry_inds with
-- 
cgit v1.2.3