diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-20 20:09:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:34 +0100 |
| commit | d4b344acb23f19b089098b7788f37ea22bc07b81 (patch) | |
| tree | 6dd26d747b259793ef6a24befd27e13234b19875 /engine/termops.mli | |
| parent | 2cd0648e003308a000f9f89c898bce4d15fc94a1 (diff) | |
Eliminating parts of the right-hand side compatibility layer
Diffstat (limited to 'engine/termops.mli')
| -rw-r--r-- | engine/termops.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/engine/termops.mli b/engine/termops.mli index 05604beda..426b5f34d 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -144,7 +144,7 @@ val pop : EConstr.t -> constr (** [subst_term_gen eq d c] replaces [d] by [Rel 1] in [c] using [eq] as equality *) val subst_term_gen : Evd.evar_map -> - (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> constr + (Evd.evar_map -> EConstr.t -> EConstr.t -> bool) -> EConstr.t -> EConstr.t -> EConstr.constr (** [replace_term_gen eq d e c] replaces [d] by [e] in [c] using [eq] as equality *) @@ -153,7 +153,7 @@ val replace_term_gen : EConstr.t -> EConstr.t -> EConstr.t -> constr (** [subst_term d c] replaces [d] by [Rel 1] in [c] *) -val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> constr +val subst_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.constr (** [replace_term d e c] replaces [d] by [e] in [c] *) val replace_term : Evd.evar_map -> EConstr.t -> EConstr.t -> EConstr.t -> constr @@ -174,7 +174,7 @@ val prod_applist : Evd.evar_map -> EConstr.t -> EConstr.t list -> EConstr.t (** Remove recursively the casts around a term i.e. [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *) -val strip_outer_cast : Evd.evar_map -> EConstr.t -> constr +val strip_outer_cast : Evd.evar_map -> EConstr.t -> EConstr.constr exception CannotFilter @@ -204,10 +204,10 @@ val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr (** Force the decomposition of a term as an applicative one *) -val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array +val decompose_app_vect : Evd.evar_map -> EConstr.t -> EConstr.constr * EConstr.constr array -val adjust_app_list_size : constr -> constr list -> constr -> constr list -> - (constr * constr list * constr * constr list) +val adjust_app_list_size : EConstr.constr -> EConstr.constr list -> EConstr.constr -> EConstr.constr list -> + (EConstr.constr * EConstr.constr list * EConstr.constr * EConstr.constr list) val adjust_app_array_size : EConstr.constr -> EConstr.constr array -> EConstr.constr -> EConstr.constr array -> (EConstr.constr * EConstr.constr array * EConstr.constr * EConstr.constr array) |