declarations eliminations / debuggae inductifs (debut)

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

1 files changed, 5 insertions, 2 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7ce0d13e8..217acdb0a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -153,8 +153,11 @@ let build_mutual lparams lnamearconstrs finite =
       mind_entry_inds = mispecvec }
     in
     States.unfreeze fs;
-    declare_mind mie;
-    pPNL(minductive_message lrecnames)
+    let sp = declare_mind mie in
+    pPNL(minductive_message lrecnames);
+    for i = 0 to List.length mispecvec - 1 do
+      declare_eliminations sp i
+    done
   with e ->
     States.unfreeze fs; raise e