From 3f286f3fcb846cac360969372d71e91c5aefe810 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 13 Apr 2020 00:47:47 +0200
Subject: Adding functions to returning the def/decl status of an inductive
 arity.

---
 pretyping/inductiveops.ml  | 8 ++++++++
 pretyping/inductiveops.mli | 4 ++++
 2 files changed, 12 insertions(+)

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 23145b1629..bd875cf68b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -245,6 +245,14 @@ let inductive_alldecls env (ind,u) =
 let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u)
 [@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"]
 
+let inductive_alltags env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  Context.Rel.to_tags mip.mind_arity_ctxt
+
+let constructor_alltags env (ind,j) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  Context.Rel.to_tags (fst mip.mind_nf_lc.(j-1))
+
 let constructor_has_local_defs env (indsp,j) =
   let (mib,mip) = Inductive.lookup_mind_specif env indsp in
   let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 1e2bba9f73..3705d39280 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -138,6 +138,10 @@ val constructor_nrealdecls : env -> constructor -> int
 val constructor_nrealdecls_env : env -> constructor -> int
 [@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"]
 
+(** @return tags of all decls: true = assumption, false = letin *)
+val inductive_alltags : env -> inductive -> bool list
+val constructor_alltags : env -> constructor -> bool list
+
 (** Is there local defs in params or args ? *)
 val constructor_has_local_defs : env -> constructor -> bool
 val inductive_has_local_defs : env -> inductive -> bool
-- 
cgit v1.2.3