@@ -215,6 +215,8 @@ extension syn ns rules =
215215 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)
216216 update ns (PIdiom fc t) = PIdiom fc $ update ns t
217217 update ns (PMetavar fc n) = PMetavar fc $ updateB ns n
218+ update ns (PProof tacs) = PProof $ map (updTactic ns) tacs
219+ update ns (PTactics tacs) = PTactics $ map (updTactic ns) tacs
218220 update ns (PDisamb nsps t) = PDisamb nsps $ update ns t
219221 update ns (PUnifyLog t) = PUnifyLog $ update ns t
220222 update ns (PNoImplicits t) = PNoImplicits $ update ns t
@@ -226,6 +228,23 @@ extension syn ns rules =
226228 -- PConstSugar probably can't contain anything substitutable, but it's hard to track
227229 update ns t = t
228230
231+ updTactic :: [(Name, SynMatch)] -> PTactic -> PTactic
232+ -- handle all the ones with Names explicitly, then use fmap for the rest with PTerms
233+ updTactic ns (Intro ns') = Intro $ map (updateB ns) ns'
234+ updTactic ns (Focus n) = Focus $ updateB ns n
235+ updTactic ns (Refine n bs) = Refine (updateB ns n) bs
236+ updTactic ns (Claim n t) = Claim (updateB ns n) (update ns t)
237+ updTactic ns (MatchRefine n) = MatchRefine (updateB ns n)
238+ updTactic ns (LetTac n t) = LetTac (updateB ns n) (update ns t)
239+ updTactic ns (LetTacTy n ty tm) = LetTacTy (updateB ns n) (update ns ty) (update ns tm)
240+ updTactic ns (ProofSearch rec prover depth top psns hints) = ProofSearch rec prover depth
241+ (fmap (updateB ns) top) (map (updateB ns) psns) (map (updateB ns) hints)
242+ updTactic ns (Try l r) = Try (updTactic ns l) (updTactic ns r)
243+ updTactic ns (TSeq l r) = TSeq (updTactic ns l) (updTactic ns r)
244+ updTactic ns (GoalType s tac) = GoalType s $ updTactic ns tac
245+ updTactic ns (TDocStr (Left n)) = TDocStr . Left $ updateB ns n
246+ updTactic ns t = fmap (update ns) t
247+
229248 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)
230249 updTacImp _ x = x
231250