From 7e35396cc95d8e82b812c7e3d40690085845bf9e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 7 Feb 2006 23:35:48 +0000
Subject: oubli de code de debugging

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8006 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/inductiveops.ml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 7c371c0119..3e43eee4dd 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -120,9 +120,6 @@ let constructor_nrealhyps env (ind,j) =
 
 let inductive_nargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  print_int mip.mind_nrealargs;
-  print_int (rel_context_length mib.mind_params_ctxt);
-  flush stdout;
   mip.mind_nrealargs + rel_context_nhyps mib.mind_params_ctxt
 
 (* Annotation for cases *)
-- 
cgit v1.2.3