From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- dev/printers.mllib | 49 ++++++++++++++++++++++++++++--------------------- 1 file changed, 28 insertions(+), 21 deletions(-) (limited to 'dev/printers.mllib') diff --git a/dev/printers.mllib b/dev/printers.mllib index ab7e9fc3..31654954 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -8,6 +8,7 @@ Hashcons CSet CMap Int +Dyn HMap Option Store @@ -18,26 +19,29 @@ Pp_control Loc CList CString +Tok Compat Flags Control Loc Serialize Stateid -Feedback -Pp -Segmenttree -Unicodetable -Unicode CObj CArray CStack Util +Pp Ppstyle -Errors +Richpp +Feedback +Segmenttree +Unicodetable +Unicode +CErrors +CWarnings Bigint -Dyn CUnix +Minisys System Envars Aux_file @@ -48,13 +52,14 @@ Rtree Heap Genarg Stateid -Ephemeron +CEphemeron Future RemoteCounter Monad Names Univ +UGraph Esubst Uint31 Sorts @@ -81,7 +86,7 @@ Nativecode Nativelib Cbytegen Environ -Closure +CClosure Reduction Nativeconv Type_errors @@ -116,17 +121,21 @@ Miscops Universes Termops Namegen +UState Evd +Sigma Glob_ops Redops +Pretype_errors +Evarutil Reductionops Inductiveops Arguments_renaming Nativenorm Retyping Cbv -Pretype_errors -Evarutil + +Evardefine Evarsolve Recordops Evarconv @@ -137,6 +146,11 @@ Find_subterm Tacred Classops Typeclasses_errors +Logic_monad +Proofview_monad +Proofview +Ftactic +Geninterp Typeclasses Detyping Indrec @@ -150,8 +164,7 @@ Library States Genprint -Tok -Lexer +CLexer Ppextend Pputils Ppannotation @@ -171,21 +184,16 @@ Implicit_quantifiers Constrintern Modintern Constrextern -Proof_type Goal Miscprint Logic Refiner Clenv Evar_refiner -Proof_errors -Logic_monad -Proofview_monad -Proofview +Refine Proof Proof_global Pfedit -Tactic_debug Decl_mode Ppconstr Pcoq @@ -195,13 +203,12 @@ Ppdecl_proof Egramml Egramcoq Tacsubst -Tacenv Trie Dn Btermdn Hints Himsg -Cerrors +ExplainErr Locality Assumptions Vernacinterp -- cgit v1.2.3