diff options
Diffstat (limited to 'engine/eConstr.mli')
| -rw-r--r-- | engine/eConstr.mli | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli index ecb36615f3..f897448557 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -224,7 +224,11 @@ 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 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 @@ -315,6 +319,9 @@ sig val to_constr : t -> Constr.t (** Physical identity. Does not care for defined evars. *) + val to_constr_array : t array -> Constr.t array + (** Physical identity. Does not care for defined evars. *) + val to_rel_decl : (t, types) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt (** Physical identity. Does not care for defined evars. *) |