From 2f5fefcd76259d5e0aee5ef5076ae4c4dd662ec1 Mon Sep 17 00:00:00 2001
From: Talia Ringer
Date: Fri, 7 Jun 2019 06:59:16 -0400
Subject: Update, expand, and document plugin tutorial 2

---
 doc/plugin_tutorial/tuto2/theories/Test.v | 19 -------------------
 1 file changed, 19 deletions(-)
 delete mode 100644 doc/plugin_tutorial/tuto2/theories/Test.v

(limited to 'doc/plugin_tutorial/tuto2/theories/Test.v')

diff --git a/doc/plugin_tutorial/tuto2/theories/Test.v b/doc/plugin_tutorial/tuto2/theories/Test.v
deleted file mode 100644
index 38e83bfff1..0000000000
--- a/doc/plugin_tutorial/tuto2/theories/Test.v
+++ /dev/null
@@ -1,19 +0,0 @@
-Declare ML Module "demo_plugin".
-
-Cmd1.
-Cmd2 With Some Terminal Parameters.
-Cmd3 42.
-Cmd4 100 200 300 400.
-Cmd5 Foo_5.
-Cmd5 Bar_5.
-Cmd6.
-Cmd7.
-Cmd7.
-Cmd7.
-
-Goal True.
-Proof.
-  tactic1.
-  tactic2 Foo_2.
-  tactic2 Bar_2.
-Abort.
-- 
cgit v1.2.3