[econstr] Add a couple of new API functions.

These are also convenient from `vernac` [to be used in future PRs].

1 files changed, 23 insertions, 0 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 53123c9334..a65b3941ef 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -770,6 +770,20 @@ let rec isArity sigma c =
   | Sort _          -> true
   | _               -> false
 
+type arity = rel_context * ESorts.t
+
+let destArity sigma =
+  let open Context.Rel.Declaration in
+  let rec prodec_rec l c =
+    match kind sigma c with
+    | Prod (x,t,c)    -> prodec_rec (LocalAssum (x,t) :: l) c
+    | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c
+    | Cast (c,_,_)      -> prodec_rec l c
+    | Sort s          -> l,s
+    | _               -> anomaly ~label:"destArity" (Pp.str "not an arity.")
+  in
+  prodec_rec []
+
 let mkProd_or_LetIn decl c =
   let open Context.Rel.Declaration in
   match decl with
@@ -817,6 +831,15 @@ let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
 let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
 let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
 
+let map_rel_context_in_env f env sign =
+  let rec aux env acc = function
+    | d::sign ->
+        aux (push_rel d env) (Context.Rel.Declaration.map_constr (f env) d :: acc) sign
+    | [] ->
+        acc
+  in
+  aux env [] (List.rev sign)
+
 let fresh_global ?loc ?rigid ?names env sigma reference =
   let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
   evd, of_constr t