aboutsummaryrefslogtreecommitdiff
path: root/printing/prettyp.ml
AgeCommit message (Expand)Author
2017-06-12[lib] Remove obsolete state-management function add_frozen_stateEmilio Jesus Gallego Arias
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Use located in misctypes.Emilio Jesus Gallego Arias
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-27Do so that "About" tells if a reference is a coercion.Hugo Herbelin
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Removing compatibility layers related to printing.Pierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Reductionops API using EConstr.Pierre-Marie Pédrot
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 18:59:04 +0000