aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--dev/base_include3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include
index c58a35748..fa6add7d3 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -15,6 +15,7 @@
#directory "printing";;
#directory "grammar";;
#directory "intf";;
+#directory "stm";;
#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
@@ -154,7 +155,7 @@ open Command
open Indschemes
open Ind_tables
open Auto_ind_decl
-open Lemmas
+(* open Lemmas *)
open Coqinit
open Coqtop
open Discharge