From 3f40ddb52ed52ea1e1939feaecf952269335500f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 25 Apr 2009 17:41:20 +0000
Subject: - Fixing #2090 (occur check missing when trying to solve evar-evar
 equation). - Adding test file related to commit 12080 (bug #2091). - Cleaning
 old parsing stuff from 8.0. - Support for camlp5 in base_include.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12106 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/base_include | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index d4366843f1..711dcb2a1e 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -14,6 +14,9 @@
 #directory "tactics";;
 #directory "translate";;
 
+#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
+#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
+
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
@@ -112,6 +115,9 @@ open Proof_type
 open Redexpr
 open Refiner
 open Tacmach
+open Decl_proof_instr
+open Tactic_debug
+open Decl_mode
 
 open Auto
 open Autorewrite
-- 
cgit v1.2.3