From c25e86e6b4e8bb694d3c8e50f04a92cc33ad807d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 24 Jul 2017 17:41:01 +0200
Subject: Turning the ltac2 subfolder into a standalone plugin.

---
 _CoqProject | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 _CoqProject

(limited to '_CoqProject')

diff --git a/_CoqProject b/_CoqProject
new file mode 100644
index 0000000000..90338abbfb
--- /dev/null
+++ b/_CoqProject
@@ -0,0 +1,28 @@
+-R theories/ Ltac2
+-I src/
+-bypass-API
+
+src/tac2expr.mli
+src/tac2env.ml
+src/tac2env.mli
+src/tac2print.ml
+src/tac2print.mli
+src/tac2intern.ml
+src/tac2intern.mli
+src/tac2interp.ml
+src/tac2interp.mli
+src/tac2entries.ml
+src/tac2entries.mli
+src/tac2core.ml
+src/tac2core.mli
+src/g_ltac2.ml4
+src/ltac2_plugin.mlpack
+
+theories/Init.v
+theories/Int.v
+theories/String.v
+theories/Array.v
+theories/Control.v
+theories/Message.v
+theories/Constr.v
+theories/Ltac2.v
-- 
cgit v1.2.3