diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /dev/printers.mllib | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
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 |