summaryrefslogtreecommitdiff
path: root/files.txt
diff options
context:
space:
mode:
authorGravatar Nicolas Braud-Santoni <nicolas@braud-santoni.eu>2016-07-23 16:21:44 -0400
committerGravatar Nicolas Braud-Santoni <nicolas@braud-santoni.eu>2016-07-23 16:21:44 -0400
commit17564e4922acda6b72bf39de7a8c23ed0c0178f6 (patch)
tree9551ca9435f64c019dbef48894f5dd0c64045f1c /files.txt
parenta77bca84565b26aeedec3b210d761240d9d261f4 (diff)
Imported Upstream version 8.5.1
Diffstat (limited to 'files.txt')
-rw-r--r--files.txt11
1 files changed, 0 insertions, 11 deletions
diff --git a/files.txt b/files.txt
deleted file mode 100644
index fb0b175..0000000
--- a/files.txt
+++ /dev/null
@@ -1,11 +0,0 @@
-AAC_coq.ml
-AAC_helper.ml
-AAC_search_monad.ml
-AAC_matcher.ml
-AAC_theory.ml
-AAC_print.ml
-AAC_rewrite.ml
-AAC.v
-Instances.v
-Tutorial.v
-Caveats.v