From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Thu, 15 Jun 2017 16:50:05 +0200
Subject: Fix a bug in cumulativity

---
 dev/base_include | 2 --
 1 file changed, 2 deletions(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index f9af0696b..8ee1cceb2 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -58,8 +58,6 @@
 
 (* Open main files *)
 
-open API
-open Grammar_API
 open Names
 open Term
 open Vars
-- 
cgit v1.2.3