aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/main.mli
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-30 13:01:48 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-01-10 18:27:28 +0100
commit8c59f1a464a446191f48358fe2484ec65ac0ef1c (patch)
tree85701335471ba6a62bc267d01747fc26c5e5c665 /checker/main.mli
parentd439c01190f45de5ac493b8f55d361503e83ad03 (diff)
Add interfaces for checker and remove dead code.
Diffstat (limited to 'checker/main.mli')
-rw-r--r--checker/main.mli10
1 files changed, 10 insertions, 0 deletions
diff --git a/checker/main.mli b/checker/main.mli
new file mode 100644
index 000000000..e1555ba2e
--- /dev/null
+++ b/checker/main.mli
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* This empty file avoids a race condition that occurs when compiling a .ml file
+ that does not have a corresponding .mli file *)