From 99638c739c57b6b2b11067eba3fe900749201d74 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Thu, 18 Jun 2026 12:39:40 +0200
Subject: [PATCH] update Tactic after changes in lambdapi

---
 Tactic.lp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Tactic.lp b/Tactic.lp
index 13f54fd..6d4597e 100644
--- a/Tactic.lp
+++ b/Tactic.lp
@@ -46,7 +46,7 @@ builtin "remove" ≔ #remove;
 constant symbol #repeat : Tactic → Tactic;
 builtin "repeat" ≔ #repeat;
 
-constant symbol #rewrite [p] : π p → Tactic;
+ symbol #rewrite : String → String → Π [a], π a → Tactic;
 builtin "rewrite" ≔ #rewrite;
 
 constant symbol #set : String → Π [a], τ a → Tactic;
@@ -70,6 +70,9 @@ builtin "try" ≔ #try;
 constant symbol #why3 : Tactic;
 builtin "why3" ≔ #why3;
 
+constant symbol #change : Tactic;
+builtin "change" ≔ #change;
+
 // defined tactics
 
 symbol nothing ≔ #try #fail;