aboutsummaryrefslogtreecommitdiff
path: root/.typerex
diff options
context:
space:
mode:
authorPierre2014-01-09 18:45:00 +0100
committerPierre2014-01-09 18:51:19 +0100
commitb9ee515a3685a606a0d33f1b06669bf7c4f617e7 (patch)
tree57c25af94723d97799d21e90cef690fb3c9d7c7b /.typerex
parentb77a894bc8efe119e6806936c8c5618cdf106834 (diff)
Goodbye typerex, Hello merlin
Diffstat (limited to '.typerex')
-rw-r--r--.typerex17
1 files changed, 0 insertions, 17 deletions
diff --git a/.typerex b/.typerex
deleted file mode 100644
index 95921c8fa2..0000000000
--- a/.typerex
+++ /dev/null
@@ -1,17 +0,0 @@
-parsing
-ide
-ide/utils
-interp
-kernel
-kernel/byterun
-lib
-library
-plugins
-pretyping
-proofs
-states
-tactics
-theories
-tools
-tools/coqdoc
-toplevel \ No newline at end of file