diff options
| author | Gaëtan Gilbert | 2020-02-09 19:49:33 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-14 16:10:09 +0100 |
| commit | faef5dcc656148273063f25716923d9bd1fe2497 (patch) | |
| tree | 2194a1c038c924da4bea8d449082fe130662af0e /pretyping/reductionops.mli | |
| parent | 90ccf8e413aea57ec670ea26174d3deffb4036aa (diff) | |
Use thunks to univ instead of lazy constr for template typing
Diffstat (limited to 'pretyping/reductionops.mli')
| -rw-r--r-- | pretyping/reductionops.mli | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index e72f5f2793..c539ec55ed 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -236,12 +236,20 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr val splay_lam : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * constr +val splay_prod_assum : env -> evar_map -> constr -> rel_context * constr + val splay_arity : env -> evar_map -> constr -> (Name.t Context.binder_annot * constr) list * ESorts.t +(** Raises [Reduction.NotArity] *) + val sort_of_arity : env -> evar_map -> constr -> ESorts.t +(** Raises [Reduction.NotArity] *) + val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr +(** Raises [Invalid_argument] *) + val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr -val splay_prod_assum : - env -> evar_map -> constr -> rel_context * constr +(** Raises [Invalid_argument] *) + type 'a miota_args = { mP : constr; (** the result type *) |