@@ -177,6 +177,7 @@ extension syn ns rules =
177177 update ns (PRef fc hls n) = case lookup n ns of
178178 Just (SynTm t) -> t
179179 _ -> PRef fc hls n
180+ update ns (PPatvar fc n) = PPatvar fc $ updateB ns n
180181 update ns (PLam fc n nfc ty sc)
181182 = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)
182183 update ns (PPi p n fc ty sc)
@@ -189,15 +190,20 @@ extension syn ns rules =
189190 = PApp fc (update ns t) (map (fmap (update ns)) args)
190191 update ns (PAppBind fc t args)
191192 = PAppBind fc (update ns t) (map (fmap (update ns)) args)
192− update ns (PCase fc c opts)
193− = PCase fc (update ns c) (map (pmap (update ns)) opts)
193+ update ns (PMatchApp fc n) = PMatchApp fc $ updateB ns n
194194 update ns (PIfThenElse fc c t f)
195195 = PIfThenElse fc (update ns c) (update ns t) (update ns f)
196+ update ns (PCase fc c opts)
197+ = PCase fc (update ns c) (map (pmap (update ns)) opts)
198+ update ns (PRewrite fc eq tm mty)
199+ = PRewrite fc (update ns eq) (update ns tm) (fmap (update ns) mty)
196200 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)
197201 update ns (PDPair fc hls p l t r)
198202 = PDPair fc hls p (update ns l) (update ns t) (update ns r)
203+ update ns (PAs fc n t) = PAs fc (updateB ns n) (update ns t)
199204 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)
200205 update ns (PHidden t) = PHidden (update ns t)
206+ update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
201207 update ns (PDoBlock ds) = PDoBlock $ map (upd ns) ds
202208 where upd :: [(Name, SynMatch)] -> PDo -> PDo
203209 upd ns (DoExp fc t) = DoExp fc (update ns t)
@@ -207,7 +213,17 @@ extension syn ns rules =
207213 = DoBindP fc (update ns i) (update ns t)
208214 (map (\(l,r) -> (update ns l, update ns r)) ts)
209215 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
210− update ns (PGoal fc r n sc) = PGoal fc (update ns r) n (update ns sc)
216+ update ns (PIdiom fc t) = PIdiom fc $ update ns t
217+ update ns (PMetavar fc n) = PMetavar fc $ updateB ns n
218+ update ns (PDisamb nsps t) = PDisamb nsps $ update ns t
219+ update ns (PUnifyLog t) = PUnifyLog $ update ns t
220+ update ns (PNoImplicits t) = PNoImplicits $ update ns t
221+ update ns (PQuasiquote tm mty) = PQuasiquote (update ns tm) (fmap (update ns) mty)
222+ update ns (PUnquote t) = PUnquote $ update ns t
223+ update ns (PQuoteName n fc) = PQuoteName (updateB ns n) fc
224+ update ns (PRunElab fc t nsp) = PRunElab fc (update ns t) nsp
225+ update ns (PConstSugar fc t) = PConstSugar fc $ update ns t
226+ -- PConstSugar probably can't contain anything substitutable, but it's hard to track
211227 update ns t = t
212228
213229 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)