diff options
Diffstat (limited to 'dev/printers.mllib')
-rw-r--r-- | dev/printers.mllib | 128 |
1 files changed, 100 insertions, 28 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 40a5a822..2f78c2e9 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -1,105 +1,166 @@ Coq_config +Terminal +Hook +Canary +Hashset +Hashcons +CSet +CMap +Int +HMap +Option +Store +Exninfo +Backtrace +IStream Pp_control -Pp +Loc Compat Flags +Control +Loc +Serialize +Stateid +Feedback +Pp Segmenttree Unicodetable -Util +Unicode Errors +CObj +CList +CString +CArray +CStack +Util Bigint -Hashcons Dyn +CUnix System Envars -Store -Gmap -Fset -Fmap -Gmapl +Aux_file Profile Explore Predicate Rtree Heap -Option -Dnet -Hashtbl_alt +Genarg +Stateid +Ephemeron +Future +RemoteCounter +Monad Names Univ Esubst +Uint31 +Sorts +Evar +Constr +Context +Vars Term Mod_subst -Sign Cbytecodes Copcodes Cemitcodes -Declarations +Nativevalues +Primitives +Nativeinstr +Future +Opaqueproof +Declareops Retroknowledge +Conv_oracle Pre_env +Nativelambda +Nativecode +Nativelib Cbytegen Environ -Conv_oracle Closure Reduction +Nativeconv Type_errors -Entries Modops Inductive Typeops +Fast_typeops Indtypes Cooking Term_typing Subtyping Mod_typing +Nativelibrary Safe_typing +Unionfind Summary Nameops Libnames +Globnames Global Nametab Libobject Lib +Loadpath Goptions Decls Heads Assumptions +Keys +Locusops +Miscops +Universes Termops Namegen Evd -Glob_term +Glob_ops +Redops Reductionops Inductiveops +Arguments_renaming +Nativenorm Retyping Cbv Pretype_errors Evarutil -Term_dnet +Evarsolve Recordops Evarconv -Arguments_renaming Typing -Pattern -Matching +Patternops +Constr_matching +Find_subterm Tacred Classops Typeclasses_errors Typeclasses Detyping Indrec +Program Coercion -Unification Cases Pretyping +Unification Declaremods +Library +States +Genprint Tok Lexer Ppextend -Genarg +Pputils +Ppstyle +Ppannotation +Stdarg +Constrarg +Constrexpr_ops +Genintern +Notation_ops Topconstr Notation Dumpglob @@ -111,13 +172,16 @@ Smartlocate Constrintern Modintern Constrextern -Tacexpr Proof_type Goal +Miscprint Logic Refiner Clenv Evar_refiner +Proof_errors +Logic_monad +Proofview_monad Proofview Proof Proof_global @@ -125,16 +189,24 @@ Pfedit Tactic_debug Decl_mode Ppconstr -Extend -Extrawit Pcoq Printer Pptactic Ppdecl_proof -Tactic_printer -Egrammar +Egramml +Egramcoq +Tacsubst +Tacenv +Trie +Dn +Btermdn +Hints Himsg Cerrors -Vernacexpr +Locality Vernacinterp +Dischargedhypsmap +Discharge +Declare +Ind_tables Top_printers |