aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.ml
Commit message (Expand)AuthorAge
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\
| * Do so that "About" tells if a reference is a coercion.Gravatar Hugo Herbelin2017-03-27
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/|
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Print the type-in-type flag in various user-facing functions.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\
| * Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
* | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Do not compose List.length with List.filter.Gravatar Guillaume Melquiond2015-12-31
|/
* Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* Printing of @{} instances for polymorphic references in Print and About.Gravatar Matthieu Sozeau2015-10-28
* Fixing printing of primitive coinductive record status.Gravatar Pierre-Marie Pédrot2015-07-09
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Do not display the status of monomorphic constants unless in universe-polymor...Gravatar Guillaume Melquiond2015-03-09
* Better English for #4070 implicit arguments message (thanks to Jason for his ...Gravatar Hugo Herbelin2015-02-21
* An answer to #4070 (message for implicit arguments of inl not clear).Gravatar Hugo Herbelin2015-02-20
* Fix issue in printing due to de Bruijn bug when constructing compatibilityGravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Move conjugate_verb_to_be next to cString.plural.Gravatar Hugo Herbelin2014-11-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Fix printing of primitive record info.Gravatar Matthieu Sozeau2014-09-29
* Print information about primitive records (Print and About).Gravatar Matthieu Sozeau2014-09-28
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Fix misleading pretty-printing of information for non-universe-polymorphicGravatar Matthieu Sozeau2014-07-24
* Missing space in pretty-printerGravatar Pierre-Marie Pédrot2014-07-21
* Unifying locate code, also making it more powerful: it is now able to findGravatar Pierre-Marie Pédrot2014-07-21
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* More complete printing of Ltac location, akin to the term-dedicated Locate co...Gravatar Pierre-Marie Pédrot2014-07-21
* Locate: also display some information about module aliasingGravatar Pierre Letouzey2014-07-09
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-23 18:35:28 +0000