From 3112d687d025a1ca7959c858e4d3c39a7c3fe892 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Jul 2000 10:10:09 +0000
Subject: 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
---
 toplevel/command.ml | 7 ++++---
 1 file 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 *)
 
-- 
cgit v1.2.3