aboutsummaryrefslogtreecommitdiff
path: root/printing/prettyp.ml
AgeCommit message (Expand)Author
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-30CLEANUP: using |> operator more consistentlyMatej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-07-06primproj: warning and avoid error.Matthieu Sozeau
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-18Print the type-in-type flag in various user-facing functions.Pierre-Marie Pédrot
2016-03-18Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-10Primitive projections: protect kernel from erroneous definitions.Matthieu Sozeau
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-31Do not compose List.length with List.filter.Guillaume Melquiond
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-28Printing of @{} instances for polymorphic references in Print and About.Matthieu Sozeau
2015-07-09Fixing printing of primitive coinductive record status.Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-03-09Do not display the status of monomorphic constants unless in universe-polymor...Guillaume Melquiond
2015-02-21Better English for #4070 implicit arguments message (thanks to Jason for his ...Hugo Herbelin
2015-02-20An answer to #4070 (message for implicit arguments of inl not clear).Hugo Herbelin
2015-01-13Fix issue in printing due to de Bruijn bug when constructing compatibilityMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:27:55 +0000