diff options
| -rw-r--r-- | _CoqProject | 2 | ||||
| -rw-r--r-- | src/Util/Tactics/NormalizeCommutativeIdentifier.v (renamed from src/Util/Tactics/RewriteWithCommutativity.v) | 0 |
2 files changed, 1 insertions, 1 deletions
diff --git a/_CoqProject b/_CoqProject index 9f814f84c..70fca8fd2 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6585,13 +6585,13 @@ src/Util/Tactics/GetGoal.v src/Util/Tactics/Head.v src/Util/Tactics/HeadUnderBinders.v src/Util/Tactics/MoveLetIn.v +src/Util/Tactics/NormalizeCommutativeIdentifier.v src/Util/Tactics/Not.v src/Util/Tactics/OnSubterms.v src/Util/Tactics/PoseTermWithName.v src/Util/Tactics/PrintContext.v src/Util/Tactics/Revert.v src/Util/Tactics/RewriteHyp.v -src/Util/Tactics/RewriteWithCommutativity.v src/Util/Tactics/RunTacticAsConstr.v src/Util/Tactics/SetEvars.v src/Util/Tactics/SetoidSubst.v diff --git a/src/Util/Tactics/RewriteWithCommutativity.v b/src/Util/Tactics/NormalizeCommutativeIdentifier.v index 00af95566..00af95566 100644 --- a/src/Util/Tactics/RewriteWithCommutativity.v +++ b/src/Util/Tactics/NormalizeCommutativeIdentifier.v |