From 801cd9cb0559d3b78216da166044bd02348ed9af Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 31 Oct 2014 17:28:42 +0100
Subject: More "open" by default for trace debugging.

---
 dev/base_include | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 7ec0bf4938..71ccea9693 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -80,6 +80,7 @@ open Pattern
 open Patternops
 open Cbv
 open Classops
+open Arguments_renaming
 open Pretyping
 open Cbv
 open Classops
@@ -103,7 +104,15 @@ open Namegen
 open Indrec
 open Typing
 open Inductiveops
+open Locusops
+open Find_subterm
 open Unification
+open Miscops
+open Miscops
+open Nativenorm
+open Typeclasses
+open Typeclasses_errors
+open Vnorm
 
 open Constrextern
 open Constrintern
@@ -123,14 +132,20 @@ open Prettyp
 open Search
 
 open Evar_refiner
+open Goal
 open Logic
 open Pfedit
+open Proof
+open Proofview
+open Proof_using
+open Proof_global
 open Proof_type
 open Redexpr
 open Refiner
 open Tacmach
-open Decl_proof_instr
 open Tactic_debug
+
+open Decl_proof_instr
 open Decl_mode
 
 open Auto
-- 
cgit v1.2.3