summaryrefslogtreecommitdiff
path: root/library/library.mllib
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
commit9043add656177eeac1491a73d2f3ab92bec0013c (patch)
tree2b0092c84bfbf718eca10c81f60b2640dc8cab05 /library/library.mllib
parenta4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff)
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'library/library.mllib')
-rw-r--r--library/library.mllib3
1 files changed, 1 insertions, 2 deletions
diff --git a/library/library.mllib b/library/library.mllib
index 92065736..e43bfb5a 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,11 +1,9 @@
-Nameops
Libnames
Globnames
Libobject
Summary
Nametab
Global
-Universes
Lib
Declaremods
Loadpath
@@ -17,3 +15,4 @@ Goptions
Decls
Heads
Keys
+Coqlib