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 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tuto0/_CoqProject')

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
-- 
cgit v1.2.3