diff options
Diffstat (limited to 'src/CoqUp/Tactics.v')
-rw-r--r-- | src/CoqUp/Tactics.v | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/src/CoqUp/Tactics.v b/src/CoqUp/Tactics.v deleted file mode 100644 index 5978d49..0000000 --- a/src/CoqUp/Tactics.v +++ /dev/null @@ -1,16 +0,0 @@ -Module Tactics. - - Ltac unfold_rec c := unfold c; fold c. - - Ltac solve_by_inverts n := - match goal with | H : ?T |- _ => - match type of T with Prop => - inversion H; - match n with S (S (?n')) => subst; try constructor; solve_by_inverts (S n') end - end - end. - - Ltac solve_by_invert := solve_by_inverts 1. - -End Tactics. -Export Tactics. |