diff options
| author | herbelin | 2005-02-18 22:07:53 +0000 |
|---|---|---|
| committer | herbelin | 2005-02-18 22:07:53 +0000 |
| commit | cd1257fcefd1f0afa09c638681f208c6949470a2 (patch) | |
| tree | 607c2a700ca45dcb19c4edd7a389e22d21ccc4c5 | |
| parent | 36e6478a343fc93b849a2019b78ef5b3d8542910 (diff) | |
Ajout splay_lambda
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6739 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 : |