From 127e40a28d2659e2e2197b87cf043a375647fe3b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 17 May 2018 17:25:28 +0200
Subject: add little test

- tests the plugin can actually be loaded (eg with the wrong DECLARE PLUGIN
  it loads but then the tactic is not in scope)
- sine is listed in _CoqProject one can open it with CoqIDE/PG and get
  the -I -R flags from the _CoqProject automatically
---
 tuto0/_CoqProject     | 4 +++-
 tuto0/theories/Demo.v | 8 ++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 tuto0/theories/Demo.v

diff --git a/tuto0/_CoqProject b/tuto0/_CoqProject
index ca0c0588a4..dd93e1fa79 100644
--- a/tuto0/_CoqProject
+++ b/tuto0/_CoqProject
@@ -2,7 +2,9 @@
 -I src
 
 theories/Loader.v
+theories/Demo.v
+
 src/tuto0_main.ml
 src/tuto0_main.mli
 src/g_tuto0.ml4
-src/tuto0_plugin.mlpack
\ No newline at end of file
+src/tuto0_plugin.mlpack
diff --git a/tuto0/theories/Demo.v b/tuto0/theories/Demo.v
new file mode 100644
index 0000000000..bdc61986af
--- /dev/null
+++ b/tuto0/theories/Demo.v
@@ -0,0 +1,8 @@
+From Tuto0 Require Import Loader.
+
+HelloWorld.
+
+Lemma test : True.
+Proof.
+hello_world.
+Abort.
-- 
cgit v1.2.3