diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-05 13:15:15 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-05 13:15:15 +0100 |
| commit | 736e86e06b5831a0dd4b6a655708b4ffd2b4ee64 (patch) | |
| tree | f1f572e011f0e5e476256d58517258774bdf149e /pretyping | |
| parent | a46a04577e34c69b42c2728ec1e0babb5be23e31 (diff) | |
| parent | 7267e31fa4456aee62a1e39dfdb7e38a8832f93f (diff) | |
Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad
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 [] |