diff options
| -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 |