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.
---
 vo.itarget | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 vo.itarget

(limited to 'vo.itarget')

diff --git a/vo.itarget b/vo.itarget
new file mode 100644
index 0000000000..776404ad79
--- /dev/null
+++ b/vo.itarget
@@ -0,0 +1 @@
+Ltac2.vo
-- 
cgit v1.2.3