From 2bd1fc392c0b22f5eaa37919c6a26330dd72c7d4 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sat, 17 Aug 2019 10:21:42 -0400
Subject: Generic traversal for Elab should visit let-bound patterns

---
 src/elab_util.sml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'src/elab_util.sml')

diff --git a/src/elab_util.sml b/src/elab_util.sml
index 0cdb9cc1..aa5bc6a4 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -541,11 +541,13 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
         and mfed ctx (dAll as (d, loc)) =
             case d of
                 EDVal (p, t, e) =>
-                S.bind2 (mfc ctx t,
-                         fn t' =>
-                            S.map2 (mfe ctx e,
-                                 fn e' =>
-                                    (EDVal (p, t', e'), loc)))
+                S.bind2 (mfp ctx p,
+                         fn p' =>
+                            S.bind2 (mfc ctx t,
+                                     fn t' =>
+                                        S.map2 (mfe ctx e,
+                                                fn e' =>
+                                                   (EDVal (p', t', e'), loc))))
               | EDValRec vis =>
                 let
                     val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis
-- 
cgit v1.2.3