diff options
| author | Matthieu Sozeau | 2014-09-10 12:54:08 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-10 13:01:24 +0200 |
| commit | c2fa953889cf7bcef9c369d175e156855ac0be2e (patch) | |
| tree | 2da6e6cd717d783d35082746d959bbb5b9edc152 | |
| parent | dcac2e58843c53137e740fc1bf324ddc16932223 (diff) | |
Fix categorization of recursive inductives.
| -rw-r--r-- | toplevel/command.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 |