diff options
| author | Pierre-Marie Pédrot | 2020-02-14 23:48:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-14 23:48:57 +0100 |
| commit | 4de476c53d85be4dd266cfe5fd5f2ddec9163a5b (patch) | |
| tree | 1f8cb4ea4350ee9dfef0d65a90aebdd3d939c1d5 /pretyping/reductionops.mli | |
| parent | bdc8e29d806ab7e9bbd0491bf237890b7934795a (diff) | |
| parent | 0f58738351db02f30ac43ec52517c54b315d5886 (diff) | |
Merge PR #11557: Use thunks to univ instead of lazy constr for template typing
Reviewed-by: ppedrot
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 *) |