diff options
| -rw-r--r-- | toplevel/command.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 7b507f5aa..08c740013 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -167,9 +167,10 @@ let build_mutual lparams lnamearconstrs finite = in let sp = declare_mind mie in if is_verbose() then pPNL(minductive_message lrecnames); - for i = 0 to List.length mispecvec - 1 do - declare_eliminations sp i - done + if finite then + for i = 0 to List.length mispecvec - 1 do + declare_eliminations sp i + done (* try to find non recursive definitions *) |