From f4161c9cc9b19f1061e1d3d6f3caf75317b18bde Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 30 Jan 2006 23:08:29 +0000
Subject: Fonctions retournant les arits des constructeurs et inductifs (suite)

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

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 59a6356ac5..7c371c0119 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -114,13 +114,16 @@ let constructor_nrealargs env (ind,j) =
 
 let constructor_nrealhyps env (ind,j) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  mip.mind_consnrealargs.(j-1) - List.length (mib.mind_params_ctxt)
+  mip.mind_consnrealargs.(j-1) - rel_context_length (mib.mind_params_ctxt)
 
 (* Length of arity (w/o local defs) *)
 
 let inductive_nargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  mip.mind_nrealargs + rel_context_length mib.mind_params_ctxt
+  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 *)
 let make_case_info env ind style pats_source =
-- 
cgit v1.2.3