diff options
| -rw-r--r-- | pretyping/reductionops.ml | 11 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 1 |
2 files changed, 12 insertions, 0 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 3b0c1d6420..a7573f5343 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -575,6 +575,17 @@ let splay_prod env sigma = in decrec env [] +let splay_lambda env sigma = + let rec decrec env m c = + let t = whd_betadeltaiota env sigma c in + match kind_of_term t with + | Lambda (n,a,c0) -> + decrec (push_rel (n,None,a) env) + ((n,a)::m) c0 + | _ -> m,t + in + decrec env [] + let splay_prod_assum env sigma = let rec prodec_rec env l c = let t = whd_betadeltaiota_nolet env sigma c in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 9f0a73d053..29a28f0f74 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -121,6 +121,7 @@ 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_lambda : env -> evar_map -> constr -> (name * constr) list * constr val splay_arity : env -> evar_map -> constr -> (name * constr) list * sorts val sort_of_arity : env -> constr -> sorts val decomp_n_prod : |