From 31e686c2904c3015eaec18ce502d4e8afe565850 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 29 Aug 2017 18:17:19 +0200
Subject: Rolling our own dynamic types for Ltac2.

This prevents careless confusions with generic arguments from Coq.
---
 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 f9fa2fafd8..92f391a085 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -1,3 +1,4 @@
+Tac2dyn
 Tac2env
 Tac2print
 Tac2intern
-- 
cgit v1.2.3