diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:43:16 +0100 |
commit | f219abfed720305c13875c3c63f9240cf63f78bc (patch) | |
tree | 69d2c026916128fdb50b8d1c0dbf1be451340d30 /dev/printers.mllib | |
parent | 476d60ef0fe0ac015c1e902204cdd7029e10ef0f (diff) | |
parent | cec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff) |
Merge tag 'upstream/8.5_beta1+dfsg'
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 |