From a581331f26d96d1a037128ae83bebd5e6c27f665 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Mar 2016 00:26:02 +0100
Subject: Creating a dedicated ltac/ folder for Hightactics.

---
 dev/base_include | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 767e023ea2..86f34b2ac9 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -17,6 +17,7 @@
 #directory "grammar";;
 #directory "intf";;
 #directory "stm";;
+#directory "ltac";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
-- 
cgit v1.2.3