4 files changed, 38 insertions, 4 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index d303038c5d..a65b3941ef 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -150,6 +150,8 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt
 type named_context = (constr, types) Context.Named.pt
 type rel_context = (constr, types) Context.Rel.pt
 
+type 'a puniverses = 'a * EInstance.t
+
 let in_punivs a = (a, EInstance.empty)
 
 let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
@@ -768,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
@@ -815,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
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f54c422adc..30de748a19 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -56,6 +56,8 @@ sig
   val is_empty : t -> bool
 end
 
+type 'a puniverses = 'a * EInstance.t
+
 (** {5 Destructors} *)
 
 val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
@@ -144,7 +146,11 @@ val isFix : Evd.evar_map -> t -> bool
 val isCoFix : Evd.evar_map -> t -> bool
 val isCase : Evd.evar_map -> t -> bool
 val isProj : Evd.evar_map -> t -> bool
+
+type arity = rel_context * ESorts.t
+val destArity : Evd.evar_map -> types -> arity
 val isArity : Evd.evar_map -> t -> bool
+
 val isVarId  : Evd.evar_map -> Id.t -> t -> bool
 val isRelN : Evd.evar_map -> int -> t -> bool
 
@@ -260,6 +266,9 @@ val lookup_rel : int -> env -> rel_declaration
 val lookup_named : variable -> env -> named_declaration
 val lookup_named_val : variable -> named_context_val -> named_declaration
 
+val map_rel_context_in_env :
+  (env -> constr -> constr) -> env -> rel_context -> rel_context
+
 (* XXX Missing Sigma proxy *)
 val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
diff --git a/engine/uState.ml b/engine/uState.ml
index 6566ad989c..6131f4c033 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -240,8 +240,8 @@ let add_constraints ctx cstrs =
       uctx_univ_variables = vars;
       uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes }
 
-(* let addconstrkey = Profile.declare_profile "add_constraints_context";; *)
-(* let add_constraints_context = Profile.profile2 addconstrkey add_constraints_context;; *)
+(* let addconstrkey = CProfile.declare_profile "add_constraints_context";; *)
+(* let add_constraints_context = CProfile.profile2 addconstrkey add_constraints_context;; *)
 
 let add_universe_constraints ctx cstrs =
   let univs, local = ctx.uctx_local in
diff --git a/engine/universes.ml b/engine/universes.ml
index 0250295fdf..30490ec56a 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -946,8 +946,8 @@ let normalize_context_set ctx us algs =
   let us = normalize_opt_subst us in
     (us, algs), (ctx', Constraint.union noneqs eqs)
 
-(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *)
-(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *)
+(* let normalize_conkey = CProfile.declare_profile "normalize_context_set" *)
+(* let normalize_context_set a b c = CProfile.profile3 normalize_conkey normalize_context_set a b c *)
 
 let is_trivial_leq (l,d,r) =
   Univ.Level.is_prop l && (d == Univ.Le || (d == Univ.Lt && Univ.Level.is_set r))