@@ -177,6 +177,7 @@ extension syn ns rules =
177 update ns (PRef fc hls n) = case lookup n ns of
177 update ns (PRef fc hls n) = case lookup n ns of
178 Just (SynTm t) -> t
178 Just (SynTm t) -> t
179 _ -> PRef fc hls n
179 _ -> PRef fc hls n
180+ update ns (PPatvar fc n) = PPatvar fc $ updateB ns n
180 update ns (PLam fc n nfc ty sc)
181 update ns (PLam fc n nfc ty sc)
181 = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)
182 = PLam fc (updateB ns n) nfc (update ns ty) (update (dropn n ns) sc)
182 update ns (PPi p n fc ty sc)
183 update ns (PPi p n fc ty sc)
@@ -189,15 +190,20 @@ extension syn ns rules =
189 = PApp fc (update ns t) (map (fmap (update ns)) args)
190 = PApp fc (update ns t) (map (fmap (update ns)) args)
190 update ns (PAppBind fc t args)
191 update ns (PAppBind fc t args)
191 = PAppBind fc (update ns t) (map (fmap (update ns)) args)
192 = PAppBind fc (update ns t) (map (fmap (update ns)) args)
192− update ns (PCase fc c opts)
193+ update ns (PMatchApp fc n) = PMatchApp fc $ updateB ns n
193− = PCase fc (update ns c) (map (pmap (update ns)) opts)
194 update ns (PIfThenElse fc c t f)
194 update ns (PIfThenElse fc c t f)
195 = PIfThenElse fc (update ns c) (update ns t) (update ns f)
195 = 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)
196 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)
200 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)
197 update ns (PDPair fc hls p l t r)
201 update ns (PDPair fc hls p l t r)
198 = PDPair fc hls p (update ns l) (update ns t) (update ns r)
202 = 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)
199 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)
204 update ns (PAlternative ms a as) = PAlternative ms a (map (update ns) as)
200 update ns (PHidden t) = PHidden (update ns t)
205 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)
201 update ns (PDoBlock ds) = PDoBlock $ map (upd ns) ds
207 update ns (PDoBlock ds) = PDoBlock $ map (upd ns) ds
202 where upd :: [(Name, SynMatch)] -> PDo -> PDo
208 where upd :: [(Name, SynMatch)] -> PDo -> PDo
203 upd ns (DoExp fc t) = DoExp fc (update ns t)
209 upd ns (DoExp fc t) = DoExp fc (update ns t)
@@ -207,7 +213,17 @@ extension syn ns rules =
207 = DoBindP fc (update ns i) (update ns t)
213 = DoBindP fc (update ns i) (update ns t)
208 (map (\(l,r) -> (update ns l, update ns r)) ts)
214 (map (\(l,r) -> (update ns l, update ns r)) ts)
209 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
215 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
211 update ns t = t
227 update ns t = t
213 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)
229 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)