Add pretty printing for Verilog integrated with CompCert

1 files changed, 16 insertions, 0 deletions

diff --git a/src/Common/Tactics.v b/src/Common/Tactics.v
new file mode 100644
index 0000000..5978d49
--- /dev/null
+++ b/src/Common/Tactics.v
@@ -0,0 +1,16 @@
+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.