diff options
| author | Enrico Tassi | 2018-01-29 16:43:28 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-03-04 17:55:50 +0100 |
| commit | 6b7139b0963523fc6d1c3bf95db4dd081b59105d (patch) | |
| tree | 1a79b1566ee32d2d99ba3a9f8c482edb07fc7bf0 /pretyping/reductionops.ml | |
| parent | 1071131805c62fb4d9bad6cf65178477cb767872 (diff) | |
reductionops: remove dead code "bind_assum"
Diffstat (limited to 'pretyping/reductionops.ml')
| -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 418ea271cd..c1441155d1 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 [] |