diff options
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 43c98bbd4..5195784a4 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Univ open Evd open Environ @@ -218,10 +217,10 @@ 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 +val splay_prod_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr +val splay_lam_n : env -> evar_map -> int -> constr -> Context.Rel.t * constr val splay_prod_assum : - env -> evar_map -> constr -> rel_context * constr + env -> evar_map -> constr -> Context.Rel.t * constr val is_sort : env -> evar_map -> types -> bool type 'a miota_args = { |