diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/reductionops.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 418ea271c..c1441155d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1484,16 +1484,12 @@ let hnf_lam_appvect env sigma t nl = let hnf_lam_applist env sigma t nl = List.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl -let bind_assum (na, t) = - (na, t) - let splay_prod env sigma = let rec decrec env m c = let t = whd_all env sigma c in match EConstr.kind sigma t with | Prod (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (bind_assum (n,a)::m) c0 + decrec (push_rel (LocalAssum (n,a)) env) ((n,a)::m) c0 | _ -> m,t in decrec env [] @@ -1503,8 +1499,7 @@ let splay_lam env sigma = let t = whd_all env sigma c in match EConstr.kind sigma t with | Lambda (n,a,c0) -> - decrec (push_rel (LocalAssum (n,a)) env) - (bind_assum (n,a)::m) c0 + decrec (push_rel (LocalAssum (n,a)) env) ((n,a)::m) c0 | _ -> m,t in decrec env [] |