aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/base_include1
-rw-r--r--dev/printers.mllib1
2 files changed, 0 insertions, 2 deletions
diff --git a/dev/base_include b/dev/base_include
index fa6add7d36..6e10dac3f9 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -155,7 +155,6 @@ open Command
open Indschemes
open Ind_tables
open Auto_ind_decl
-(* open Lemmas *)
open Coqinit
open Coqtop
open Discharge
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 5a9acb6dd4..2eae9d5985 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -194,4 +194,3 @@ Discharge
Declare
Ind_tables
Top_printers
-