1 files changed, 27 insertions, 9 deletions

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 882dfe2848..0d038e9a67 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -20,6 +20,8 @@ type t = Evd.econstr
 type types = t
 type constr = t
 type existential = t pexistential
+type case_return = t pcase_return
+type case_branch = t pcase_branch
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
@@ -58,6 +60,9 @@ sig
   val is_empty : t -> bool
 end
 
+type case_invert = t pcase_invert
+type case = (t, t, EInstance.t) pcase
+
 type 'a puniverses = 'a * EInstance.t
 
 (** {5 Destructors} *)
@@ -128,7 +133,7 @@ val mkIndU : inductive * EInstance.t -> t
 val mkConstruct : constructor -> t
 val mkConstructU : constructor * EInstance.t -> t
 val mkConstructUi : (inductive * EInstance.t) * int -> t
-val mkCase : case_info * t * (t,EInstance.t) case_invert * t * t array -> t
+val mkCase : case -> t
 val mkFix : (t, t) pfixpoint -> t
 val mkCoFix : (t, t) pcofixpoint -> t
 val mkArrow : t -> Sorts.relevance  -> t -> t
@@ -199,7 +204,7 @@ val destConst : Evd.evar_map -> t -> Constant.t * EInstance.t
 val destEvar : Evd.evar_map -> t -> t pexistential
 val destInd : Evd.evar_map -> t -> inductive * EInstance.t
 val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
-val destCase : Evd.evar_map -> t -> case_info * t * (t,EInstance.t) case_invert * t * t array
+val destCase : Evd.evar_map -> t -> case
 val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
@@ -250,14 +255,12 @@ val compare_constr : Evd.evar_map -> (t -> t -> bool) -> t -> t -> bool
 (** {6 Iterators} *)
 
 val map : Evd.evar_map -> (t -> t) -> t -> t
-val map_user_view : Evd.evar_map -> (t -> t) -> t -> t
 val map_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> t) -> 'a -> t -> t
-val map_under_context : (t -> t) -> int -> t -> t
-val map_branches : (t -> t) -> case_info -> t array -> t array
-val map_return_predicate : (t -> t) -> case_info -> t -> t
+val map_branches : (t -> t) -> case_branch array -> case_branch array
+val map_return_predicate : (t -> t) -> case_return -> case_return
 val iter : Evd.evar_map -> (t -> unit) -> t -> unit
 val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
-val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
+val iter_with_full_binders : Environ.env -> Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
 val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
 
 (** Gather the universes transitively used in the term, including in the
@@ -337,6 +340,21 @@ val fresh_global :
 val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
 [@@ocaml.deprecated "Use [EConstr.isRefX] instead."]
 
+val expand_case : Environ.env -> Evd.evar_map ->
+  case -> (case_info * t * case_invert * t * t array)
+
+val annotate_case : Environ.env -> Evd.evar_map -> case ->
+  case_info * EInstance.t * t array * (rel_context * t) * case_invert * t * (rel_context * t) array
+(** Same as above, but doesn't turn contexts into binders *)
+
+val expand_branch : Environ.env -> Evd.evar_map ->
+  EInstance.t -> t array -> constructor -> case_branch -> rel_context
+(** Given a universe instance and parameters for the inductive type,
+    constructs the typed context in which the branch lives. *)
+
+val contract_case : Environ.env -> Evd.evar_map ->
+  (case_info * t * case_invert * t * t array) -> case
+
 (** {5 Extra} *)
 
 val of_existential : Constr.existential -> existential
@@ -345,7 +363,7 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, typ
 
 val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
 
-val of_case_invert : (Constr.t,Univ.Instance.t) case_invert -> (t,EInstance.t) case_invert
+val of_case_invert : Constr.case_invert -> case_invert
 
 (** {5 Unsafe operations} *)
 
@@ -371,7 +389,7 @@ sig
   val to_instance : EInstance.t -> Univ.Instance.t
   (** Physical identity. Does not care for normalization. *)
 
-  val to_case_invert : (t,EInstance.t) case_invert -> (Constr.t,Univ.Instance.t) case_invert
+  val to_case_invert : case_invert -> Constr.case_invert
 
   val eq : (t, Constr.t) eq
   (** Use for transparent cast between types. *)