Moved rule instantiation related types to corresponding package (and …

…gave the package a better name)
Drodt · Jan 15, 2025 · 8cc036a · 8cc036a
1 parent e6ba6a3
commit 8cc036a
Show file tree

Hide file tree

Showing 107 changed files with 222 additions and 211 deletions.
diff --git a/...e.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java b/...e.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java
@@ -21,7 +21,7 @@
 import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil;
 
 import org.key_project.logic.Name;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.Rule;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;

diff --git a/...lic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java b/...lic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java
@@ -37,8 +37,8 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.op.SortedOperator;
 import org.key_project.logic.sort.Sort;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate;
 import org.key_project.prover.sequent.PosInOccurrence;

diff --git a/...ution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java b/...ution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java
@@ -13,7 +13,7 @@
 import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil;
 
 import org.key_project.logic.Name;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 
 /**
  * {@link Strategy} used to simplify {@link Term}s in side proofs.

diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java b/key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java
@@ -13,10 +13,10 @@
 import de.uka.ilkd.key.rule.match.vm.VMTacletMatcher;
 
 import org.key_project.logic.Name;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
-import org.key_project.prover.rules.AssumesMatchResult;
-import org.key_project.prover.rules.inst.SVInstantiations;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesMatchResult;
+import org.key_project.prover.rules.instantiation.SVInstantiations;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableArray;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/SearchNode.java b/key.core/src/main/java/de/uka/ilkd/key/api/SearchNode.java
@@ -5,8 +5,8 @@
 
 import de.uka.ilkd.key.logic.Term;
 
-import org.key_project.prover.rules.MatchConditions;
-import org.key_project.prover.rules.inst.SVInstantiations;
+import org.key_project.prover.rules.instantiation.MatchConditions;
+import org.key_project.prover.rules.instantiation.SVInstantiations;
 import org.key_project.prover.sequent.SequentFormula;
 
 /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java
@@ -22,8 +22,8 @@
 import de.uka.ilkd.key.strategy.FocussedBreakpointRuleApplicationManager;
 import de.uka.ilkd.key.strategy.FocussedRuleApplicationManager;
 
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletAssumesModel.java b/key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletAssumesModel.java
@@ -22,8 +22,8 @@
 import de.uka.ilkd.key.util.RecognitionException;
 
 import org.key_project.logic.LogicServices;
-import org.key_project.prover.rules.AssumesFormulaInstDirect;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableList;
 

diff --git a/...e/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java b/...e/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java
@@ -16,8 +16,8 @@
 import de.uka.ilkd.key.rule.inst.SortException;
 
 import org.key_project.logic.Namespace;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;

diff --git a/.../java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java b/.../java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java
@@ -13,7 +13,7 @@
 import de.uka.ilkd.key.util.properties.Properties;
 
 import org.key_project.logic.LogicServices;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.Semisequent;
 import org.key_project.prover.sequent.SequentChangeInfo;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
@@ -17,8 +17,8 @@
 import de.uka.ilkd.key.rule.inst.*;
 
 import org.key_project.logic.PosInTerm;
-import org.key_project.prover.rules.inst.InstantiationEntry;
-import org.key_project.prover.rules.inst.ListInstantiation;
+import org.key_project.prover.rules.instantiation.InstantiationEntry;
+import org.key_project.prover.rules.instantiation.ListInstantiation;
 import org.key_project.prover.sequent.*;
 import org.key_project.util.collection.*;
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
@@ -57,9 +57,9 @@
 import org.key_project.logic.op.Function;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
-import org.key_project.prover.rules.AssumesFormulaInstDirect;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java
@@ -48,11 +48,11 @@
 import org.key_project.logic.PosInTerm;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
-import org.key_project.prover.rules.AssumesFormulaInstDirect;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.RuleApp;
-import org.key_project.prover.rules.inst.InstantiationEntry;
+import org.key_project.prover.rules.instantiation.InstantiationEntry;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/replay/AbstractProofReplayer.java
@@ -26,9 +26,9 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.PosInTerm;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.AssumesFormulaInstDirect;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.Semisequent;
 import org.key_project.prover.sequent.Sequent;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/AssumesFormulaInstantiationCache.java b/key.core/src/main/java/de/uka/ilkd/key/rule/AssumesFormulaInstantiationCache.java
@@ -7,7 +7,7 @@
 import java.util.concurrent.locks.ReentrantReadWriteLock.ReadLock;
 import java.util.concurrent.locks.ReentrantReadWriteLock.WriteLock;
 
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.Semisequent;
 import org.key_project.util.LRUCache;
 import org.key_project.util.collection.ImmutableArray;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java b/key.core/src/main/java/de/uka/ilkd/key/rule/EqualityModuloProofIrrelevancy.java
@@ -16,7 +16,7 @@
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 
 import org.key_project.logic.sort.Sort;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.EqualsModProofIrrelevancyUtil;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/IfMatchResult.java b/key.core/src/main/java/de/uka/ilkd/key/rule/IfMatchResult.java
@@ -6,7 +6,7 @@
 
 import de.uka.ilkd.key.util.Debug;
 
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.util.collection.ImmutableList;
 
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/MatchConditions.java b/key.core/src/main/java/de/uka/ilkd/key/rule/MatchConditions.java
@@ -13,7 +13,7 @@
 /**
  * Simple container class containing the information resulting from a Taclet.match-call
  */
-public class MatchConditions extends org.key_project.prover.rules.MatchConditions {
+public class MatchConditions extends org.key_project.prover.rules.instantiation.MatchConditions {
 
     public static final MatchConditions EMPTY_MATCHCONDITIONS =
         new MatchConditions(SVInstantiations.EMPTY_SVINSTANTIATIONS, RenameTable.EMPTY_TABLE);
@@ -40,7 +40,7 @@ public SVInstantiations getInstantiations() {
 
     @Override
     public MatchConditions setInstantiations(
-            org.key_project.prover.rules.inst.SVInstantiations p_instantiations) {
+            org.key_project.prover.rules.instantiation.SVInstantiations p_instantiations) {
         if (instantiations == p_instantiations) {
             return this;
         } else {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/NoPosTacletApp.java
@@ -13,9 +13,9 @@
 import de.uka.ilkd.key.util.Debug;
 
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
-import org.key_project.prover.rules.MatchConditions;
-import org.key_project.prover.rules.inst.SVInstantiations;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.MatchConditions;
+import org.key_project.prover.rules.instantiation.SVInstantiations;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
@@ -245,8 +245,8 @@ public TacletApp setMatchConditions(MatchConditions mc, Services services) {
      * metavariables and if formula instantiations given and forget the old ones
      */
     @Override
-    protected TacletApp setAllInstantiations(org.key_project.prover.rules.MatchConditions mc,
-            ImmutableList<AssumesFormulaInstantiation> assumesInstantiations, Services services) {
+    protected TacletApp setAllInstantiations(MatchConditions mc,
+                                             ImmutableList<AssumesFormulaInstantiation> assumesInstantiations, Services services) {
         return createNoPosTacletApp(taclet(), mc.getInstantiations(), assumesInstantiations,
             services);
     }

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java
@@ -35,8 +35,8 @@
 
 import org.key_project.logic.Name;
 import org.key_project.logic.PosInTerm;
-import org.key_project.prover.rules.AssumesFormulaInstDirect;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstDirect;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.rules.RuleSet;
 import org.key_project.prover.sequent.*;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/PosTacletApp.java
@@ -12,9 +12,9 @@
 import de.uka.ilkd.key.util.Debug;
 
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
-import org.key_project.prover.rules.MatchConditions;
-import org.key_project.prover.rules.inst.SVInstantiations;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.MatchConditions;
+import org.key_project.prover.rules.instantiation.SVInstantiations;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
@@ -231,9 +231,9 @@ public TacletApp setMatchConditions(MatchConditions mc, Services services) {
      * metavariables and if formula instantiations given and forget the old ones
      */
     @Override
-    protected TacletApp setAllInstantiations(org.key_project.prover.rules.MatchConditions mc,
-            ImmutableList<AssumesFormulaInstantiation> assumesInstantiations,
-            Services services) {
+    protected TacletApp setAllInstantiations(MatchConditions mc,
+                                             ImmutableList<AssumesFormulaInstantiation> assumesInstantiations,
+                                             Services services) {
         return createPosTacletApp((FindTaclet) taclet(),
             mc.getInstantiations(), assumesInstantiations,
             posInOccurrence(), services);

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAppUtil.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RuleAppUtil.java
@@ -12,8 +12,8 @@
 import de.uka.ilkd.key.smt.SMTRuleApp;
 
 import org.key_project.logic.PosInTerm;
-import org.key_project.prover.rules.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
+import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
 import org.key_project.prover.rules.RuleApp;
 import org.key_project.prover.sequent.PosInOccurrence;
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java b/key.core/src/main/java/de/uka/ilkd/key/rule/TacletApp.java
@@ -27,8 +27,8 @@
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.*;
-import org.key_project.prover.rules.MatchConditions;
-import org.key_project.prover.rules.inst.SVInstantiations;
+import org.key_project.prover.rules.instantiation.*;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.sequent.*;
 import org.key_project.util.collection.*;
 
@@ -816,7 +816,7 @@ public TacletApp addInstantiation(SchemaVariable sv, Name name, Services service
      * metavariables and if formula instantiations given and forget the old ones
      */
     protected abstract TacletApp setAllInstantiations(
-            org.key_project.prover.rules.MatchConditions mc,
+            MatchConditions mc,
             ImmutableList<AssumesFormulaInstantiation> ifInstantiations, Services services);
 
     /**
@@ -894,7 +894,7 @@ private ImmutableList<TacletApp> findIfFormulaInstantiationsHelp(
             ImmutableArray<AssumesFormulaInstantiation> instSucc,
             ImmutableArray<AssumesFormulaInstantiation> instAntec,
             ImmutableList<AssumesFormulaInstantiation> instAlreadyMatched,
-            org.key_project.prover.rules.MatchConditions matchCond,
+            MatchConditions matchCond,
             Services services) {
 
         while (ruleSuccTail.isEmpty()) {
@@ -921,7 +921,7 @@ private ImmutableList<TacletApp> findIfFormulaInstantiationsHelp(
         // For each matching formula call the method again to match
         // the remaining terms
         ImmutableList<TacletApp> res = ImmutableSLList.nil();
-        Iterator<org.key_project.prover.rules.MatchConditions> itMC =
+        Iterator<MatchConditions> itMC =
             mr.matchConditions().iterator();
         ruleSuccTail = ruleSuccTail.tail();
         for (final AssumesFormulaInstantiation instantiationCandidate : mr.candidates()) {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java b/key.core/src/main/java/de/uka/ilkd/key/rule/VariableConditionAdapter.java
@@ -9,7 +9,7 @@
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 
 /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ApplyUpdateOnRigidCondition.java
@@ -14,7 +14,7 @@
 import org.key_project.logic.Name;
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableSet;

diff --git a/...re/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java b/...re/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessElementariesCondition.java
@@ -18,7 +18,7 @@
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/DropEffectlessStoresCondition.java
@@ -13,7 +13,7 @@
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.Function;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableSet;

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/EqualUniqueCondition.java
@@ -13,7 +13,7 @@
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.Function;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java
@@ -15,7 +15,7 @@
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 
 /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java
@@ -21,7 +21,7 @@
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 
 /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/IsLabeledCondition.java
@@ -14,7 +14,7 @@
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 
 /**

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/JavaTypeToSortCondition.java
@@ -19,7 +19,7 @@
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java b/key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java
@@ -22,7 +22,7 @@
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.SyntaxElement;
 import org.key_project.logic.op.sv.SchemaVariable;
-import org.key_project.prover.rules.MatchConditions;
+import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.VariableCondition;
 
 /**