diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 4263aec53..60c111370 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -154,9 +154,9 @@ val hnf_lam_app : env -> evar_map -> constr -> constr -> constr val hnf_lam_appvect : env -> evar_map -> constr -> constr array -> constr val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr -val splay_prod : env -> evar_map -> constr -> (name * constr) list * constr -val splay_lam : env -> evar_map -> constr -> (name * constr) list * constr -val splay_arity : env -> evar_map -> constr -> (name * constr) list * sorts +val splay_prod : env -> evar_map -> constr -> (Name.t * constr) list * constr +val splay_lam : env -> evar_map -> constr -> (Name.t * constr) list * constr +val splay_arity : env -> evar_map -> constr -> (Name.t * constr) list * sorts val sort_of_arity : env -> evar_map -> constr -> sorts val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr |