From 7e67bba64e1b59be2acf5997157bff10581d28f2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 1 Aug 2014 15:16:42 +0200
Subject: Continuing (incomplete) cleaning of Inductiveops.

---
 parsing/g_xml.ml4          |  2 +-
 pretyping/inductiveops.ml  | 10 ++++++++++
 pretyping/inductiveops.mli |  4 ++++
 3 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 621aab8a03..f639ee7c55 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -147,7 +147,7 @@ let compute_branches_lengths ind =
   mip.Declarations.mind_consnrealdecls
 
 let compute_inductive_ndecls ind =
-  snd (Inductiveops.inductive_ndecls ind)
+  Inductiveops.inductive_nrealdecls ind
 
 (* Interpreting constr as a glob_constr *)
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index ed243bebe6..dee22cb173 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -176,6 +176,16 @@ let constructor_nrealdecls_env env (ind,j) = (* TOCHANGE en decls *)
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_consnrealdecls.(j-1)
 
+(* Length of arity, excluding params, excluding local defs *)
+
+let inductive_nrealargs ind =
+  let (_,mip) = Global.lookup_inductive ind in
+  mip.mind_nrealargs
+
+let inductive_nrealargs_env env ind =
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_nrealargs
+
 (* Length of arity, excluding params, including local defs *)
 
 let inductive_nrealdecls ind =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 10ff968cf8..cefd5bd9da 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -66,6 +66,10 @@ val constructors_nrealargs_env : env -> inductive -> int array
 val constructors_nrealdecls : inductive -> int array
 val constructors_nrealdecls_env : env -> inductive -> int array
 
+(** @return the arity, excluding params, excluding local defs *)
+val inductive_nrealargs : inductive -> int
+val inductive_nrealargs_env : env -> inductive -> int
+
 (** @return the arity, excluding params, including local defs *)
 val inductive_nrealdecls : inductive -> int
 val inductive_nrealdecls_env : env -> inductive -> int
-- 
cgit v1.2.3