Remove now-unused @axiom macro

LS-Lab · Sep 12, 2024 · 06ffa05 · 06ffa05
1 parent 0a1c16e
commit 06ffa05
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 237 deletions.
diff --git a/keymaerax-macros/src/main/scala/org/keymaerax/btactics/macros/AnnotationCommon.scala b/keymaerax-macros/src/main/scala/org/keymaerax/btactics/macros/AnnotationCommon.scala
@@ -194,17 +194,6 @@ object AnnotationCommon {
     }
   }
 
-  def astForUnifier(unifier: Unifier)(implicit c: blackbox.Context): c.universe.Tree = {
-    import c.universe._
-    unifier match {
-      case Unifier.Full => q"org.keymaerax.btactics.macros.Unifier.Full"
-      case Unifier.Linear => q"org.keymaerax.btactics.macros.Unifier.Linear"
-      case Unifier.Surjective => q"org.keymaerax.btactics.macros.Unifier.Surjective"
-      case Unifier.SurjectiveLinear => q"org.keymaerax.btactics.macros.Unifier.SurjectiveLinear"
-      case Unifier.SurjectiveLinearPretend => q"org.keymaerax.btactics.macros.Unifier.SurjectiveLinearPretend"
-    }
-  }
-
   /** Elaborate the display formula from a raw unicode string that may contain HTML tags to HTML. */
   // TODO Figure out how to get rid of this
   def renderDisplayFormula(displayFormula: String) = displayFormula

diff --git a/keymaerax-macros/src/main/scala/org/keymaerax/btactics/macros/Axiom.scala b/keymaerax-macros/src/main/scala/org/keymaerax/btactics/macros/Axiom.scala