aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/prettyp.ml
Commit message (Expand)AuthorAge
* 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
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fix output test-suite 'simpl tactic' -> 'reduction tactics'Gravatar Pierre Boutillier2014-02-28
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Simpl_behaviour becomes Reductionops.ReductionBehaviourGravatar Pierre Boutillier2014-02-24
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Prettyp: avoid useless "let module"Gravatar letouzey2013-09-19
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Added printing of instance priority to the Print Instances command.Gravatar ppedrot2013-08-01
* Lib.contents () instead of Lib.contents_after NoneGravatar letouzey2013-07-17
* Now printing body of abbreviations (i.e. notation with a name) withGravatar herbelin2013-05-05
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Restrict (try...with...) to avoid catching critical exn (part 5)Gravatar letouzey2013-03-13
* More monomorphization.Gravatar ppedrot2013-03-05
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18