Bug: on tentait de déclarer un schéma d'induction pour un coinductif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@539 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 3 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7b507f5aa2..08c7400139 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 *)