summaryrefslogtreecommitdiff
path: root/dev/printers.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'dev/printers.mllib')
-rw-r--r--dev/printers.mllib133
1 files changed, 133 insertions, 0 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
new file mode 100644
index 00000000..e8ec10c5
--- /dev/null
+++ b/dev/printers.mllib
@@ -0,0 +1,133 @@
+Coq_config
+
+Pp_control
+Pp
+Compat
+Flags
+Segmenttree
+Unicodetable
+Util
+Bigint
+Hashcons
+Dyn
+System
+Envars
+Bstack
+Edit
+Gset
+Gmap
+Fset
+Fmap
+Tlm
+Gmapl
+Profile
+Explore
+Predicate
+Rtree
+Heap
+Option
+Dnet
+
+Names
+Univ
+Esubst
+Term
+Mod_subst
+Sign
+Cbytecodes
+Copcodes
+Cemitcodes
+Declarations
+Retroknowledge
+Pre_env
+Cbytegen
+Environ
+Conv_oracle
+Closure
+Reduction
+Type_errors
+Entries
+Modops
+Inductive
+Typeops
+Indtypes
+Cooking
+Term_typing
+Subtyping
+Mod_typing
+Safe_typing
+
+Summary
+Nameops
+Libnames
+Global
+Nametab
+Libobject
+Lib
+Goptions
+Decls
+Heads
+Termops
+Namegen
+Evd
+Rawterm
+Reductionops
+Inductiveops
+Retyping
+Cbv
+Pretype_errors
+Evarutil
+Term_dnet
+Recordops
+Evarconv
+Typing
+Pattern
+Matching
+Tacred
+Classops
+Typeclasses_errors
+Typeclasses
+Detyping
+Indrec
+Coercion
+Unification
+Cases
+Pretyping
+Clenv
+
+Lexer
+Ppextend
+Genarg
+Topconstr
+Notation
+Dumpglob
+Reserve
+Impargs
+Constrextern
+Syntax_def
+Implicit_quantifiers
+Smartlocate
+Constrintern
+Proof_trees
+Tacexpr
+Proof_type
+Logic
+Refiner
+Evar_refiner
+Pfedit
+Tactic_debug
+Decl_mode
+Ppconstr
+Extend
+Extrawit
+Pcoq
+Printer
+Pptactic
+Ppdecl_proof
+Tactic_printer
+Egrammar
+Himsg
+Cerrors
+Vernacexpr
+Vernacinterp
+Top_printers