From 94f4ade387013a2e3fe8d1042fbd152088ce1daa Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 3 Oct 2016 14:46:58 +0200
Subject: Introduction of the Ltac2 plugin.

For now, it is only a simple mini-ML whose effects are the proofview monad.
There is no facility to manipulate terms nor any hardwired tactic.

Pattern-matching is restricted to superficial constructors, the language is
lacking a lot of user-friendly interfaces, the grammar is crappy, and much
more.
---
 ltac2_plugin.mlpack | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 ltac2_plugin.mlpack

(limited to 'ltac2_plugin.mlpack')

diff --git a/ltac2_plugin.mlpack b/ltac2_plugin.mlpack
new file mode 100644
index 0000000000..561bd0eb0a
--- /dev/null
+++ b/ltac2_plugin.mlpack
@@ -0,0 +1,6 @@
+Tac2env
+Tac2intern
+Tac2interp
+Tac2entries
+Tac2core
+G_ltac2
-- 
cgit v1.2.3