From d4172d2c7a48d932b42248fe57c6c2a87ac57e30 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 25 Oct 2017 12:13:27 +0200
Subject: Stubs for goal matching: quotation and matching function.

---
 src/ltac2_plugin.mlpack | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/ltac2_plugin.mlpack')

diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index a2237f4d26..40b91e4b53 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -6,6 +6,7 @@ Tac2intern
 Tac2interp
 Tac2entries
 Tac2quote
+Tac2match
 Tac2core
 Tac2tactics
 Tac2stdlib
-- 
cgit v1.2.3