summaryrefslogtreecommitdiff
path: root/checker/check.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'checker/check.mllib')
-rw-r--r--checker/check.mllib39
1 files changed, 34 insertions, 5 deletions
diff --git a/checker/check.mllib b/checker/check.mllib
index 08dd78bc..22df3756 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,22 +1,49 @@
Coq_config
+
+Hook
+Canary
+Hashset
+Hashcons
+CSet
+CMap
+Int
+HMap
+Option
+Store
+Exninfo
+Backtrace
+Flags
+Control
Pp_control
+Loc
+Serialize
+Stateid
+Feedback
Pp
-Compat
-Flags
Segmenttree
Unicodetable
+Unicode
+Errors
+CObj
+CList
+CString
+CArray
+CStack
Util
-Option
-Hashcons
+Ephemeron
+Future
+CUnix
System
+Profile
+RemoteCounter
Envars
Predicate
Rtree
Names
Univ
Esubst
-Validate
Term
+Print
Declarations
Environ
Closure
@@ -29,6 +56,8 @@ Indtypes
Subtyping
Mod_checking
Safe_typing
+Values
+Validate
Check
Check_stat
Checker