aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorEnrico Tassi2021-01-05 11:34:35 +0100
committerEnrico Tassi2021-01-27 09:45:49 +0100
commit4264aec518d5407f345c58e18e014e15e9ae96af (patch)
tree03209892ae2549f171af39efa5d6925b745d54ec /kernel/type_errors.mli
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 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions