aboutsummaryrefslogtreecommitdiff
path: root/printing/prettyp.ml
AgeCommit message (Expand)Author
2014-11-13Move conjugate_verb_to_be next to cString.plural.Hugo Herbelin
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-09-29Fix printing of primitive record info.Matthieu Sozeau
2014-09-28Print information about primitive records (Print and About).Matthieu Sozeau
2014-09-12Referring to evars by names. Added a parser for evars (but parsing ofHugo Herbelin
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-24Fix misleading pretty-printing of information for non-universe-polymorphicMatthieu Sozeau
2014-07-21Missing space in pretty-printerPierre-Marie Pédrot
2014-07-21Unifying locate code, also making it more powerful: it is now able to findPierre-Marie Pédrot
2014-07-21Adding a new "Locate Term" command, distinct from the raw "Locate" command.Pierre-Marie Pédrot
2014-07-21More complete printing of Ltac location, akin to the term-dedicated Locate co...Pierre-Marie Pédrot
2014-07-09Locate: also display some information about module aliasingPierre Letouzey
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-28Fix output test-suite 'simpl tactic' -> 'reduction tactics'Pierre Boutillier
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-09-19Prettyp: avoid useless "let module"letouzey
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-08-08State Transaction Machinegareuselesinge
2013-08-01Added printing of instance priority to the Print Instances command.ppedrot
2013-07-17Lib.contents () instead of Lib.contents_after Noneletouzey
2013-05-05Now printing body of abbreviations (i.e. notation with a name) withherbelin
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
2013-03-05More monomorphization.ppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-21Print univ constraints generated by a constant or inductive (when flag is set)barras
2012-11-13Added a CString module.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-07-20Fixing test-suitepboutill
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-12Fixing test-suite after last storm in Pp.pboutill
2012-05-29place all pretty-printing files in new dir printing/letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 21:21:30 +0000