aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorEnrico Tassi2021-01-05 11:34:35 +0100
committerEnrico Tassi2021-01-27 09:45:49 +0100
commit4264aec518d5407f345c58e18e014e15e9ae96af (patch)
tree03209892ae2549f171af39efa5d6925b745d54ec /dev/base_include
parent4390b6907b3d07793c2e8f9e7ad3cc38d9488711 (diff)
[sysinit] new component for system initialization
This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml
Diffstat (limited to 'dev/base_include')
-rw-r--r--dev/base_include1
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include
index daee2d97c5..f375a867bc 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -134,7 +134,6 @@ open ComDefinition
open Indschemes
open Ind_tables
open Auto_ind_decl
-open Coqinit
open Coqtop
open Himsg
open Metasyntax