From 5cf1b34cef3280bb38804c9f17c6ff2b3c5ce467 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Jun 2014 19:30:09 +0200
Subject: More open in base_include

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

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index 6e10dac3f9..a5ccf24aad 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -55,6 +55,8 @@
 
 open Names
 open Term
+open Vars
+open Context
 open Typeops
 open Term_typing
 open Univ
-- 
cgit v1.2.3