From 5101fb3eb5230b233bbbbf2c4691b0a06552123f Mon Sep 17 00:00:00 2001
From: Robby <robby@santoslab.org>
Date: Fri, 9 Feb 2024 16:06:57 -0600
Subject: [PATCH] Rewriting system.

---
 library/shared/src/main/scala/org/sireum/contract.scala      | 1 +
 library/shared/src/main/scala/org/sireum/justification.scala | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/library/shared/src/main/scala/org/sireum/contract.scala b/library/shared/src/main/scala/org/sireum/contract.scala
index 20f0ca7d..e48138f8 100644
--- a/library/shared/src/main/scala/org/sireum/contract.scala
+++ b/library/shared/src/main/scala/org/sireum/contract.scala
@@ -1670,6 +1670,7 @@ trait contract {
 
   implicit def $toB(state: Contract.StateCont): B = ???
 
+  implicit def $toSequent(b: Boolean): Contract.SequentBuilder = ???
   implicit def $toSequent(bs: (B, B)): Contract.SequentBuilder = ???
   implicit def $toSequent(bs: (B, B, B)): Contract.SequentBuilder = ???
   implicit def $toSequent(bs: (B, B, B, B)): Contract.SequentBuilder = ???
diff --git a/library/shared/src/main/scala/org/sireum/justification.scala b/library/shared/src/main/scala/org/sireum/justification.scala
index 102475d5..d5ba9e46 100644
--- a/library/shared/src/main/scala/org/sireum/justification.scala
+++ b/library/shared/src/main/scala/org/sireum/justification.scala
@@ -55,7 +55,7 @@ object justification {
 
   @just def Admit: Unit = $
 
-  @just def Rewrite(rs: RS): Unit = $
+  @just def Rewrite(rs: RS, from: StepId): Unit = $
 
   object natded {