aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/cpretty.mll
Commit message (Expand)AuthorAge
* coqdoc: Support comments in verbatim outputGravatar Tej Chajed2017-08-29
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\
| * Output a break before a list only if there was an empty line (bug #4606).Gravatar Guillaume Melquiond2016-08-16
* | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2016-06-03
|\|
| * Fix proof terminators not being detected in presence of curly brackets (bug #...Gravatar Guillaume Melquiond2016-06-03
| * Make "coqdoc -g --parse-comments" behave properly (bug #4773).Gravatar Guillaume Melquiond2016-06-03
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Support "Functional Scheme" in coqdoc. (Fix bug #4382)Gravatar Guillaume Melquiond2015-10-23
* Avoid outputting stray "Local" keywords in HTML documentation.Gravatar Guillaume Melquiond2015-04-02
* Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307)Gravatar Guillaume Melquiond2015-02-11
* Update headers.Gravatar Maxime Dénès2015-01-12
* Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug #38...Gravatar Guillaume Melquiond2015-01-06
* Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers.Gravatar Hugo Herbelin2014-10-22
* Add a [Variant] declaration which allows to write non-recursive variant types.Gravatar Arnaud Spiwack2014-09-04
* Recognize Parameters as a command in coqdoc. (Fix for bug #3279)Gravatar Guillaume Melquiond2014-04-28
* Fixing coqdoc bug #3292 (unfortunate collision betweens the relativeGravatar Hugo Herbelin2014-04-28
* Prevent verbatim text from leaking out of comments. (See bug #2882)Gravatar Guillaume Melquiond2014-04-04
* Set officially the minimal OCaml requirement to 3.12.1Gravatar Pierre Letouzey2014-03-02
* still some more dead code removalGravatar letouzey2012-10-06
* Updating headers.Gravatar herbelin2012-08-08
* Coqdoc inlined verbatim_char in latexGravatar pboutill2012-08-06
* Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) markup/typese...Gravatar pboutill2012-08-06
* Various minor fixes to coqdoc from A. Chlipala.Gravatar msozeau2012-07-18
* Fix handling of space after "Notation" or "where", add missing keywords.Gravatar msozeau2012-02-16
* Coqdoc: Fixing missing newline when using "Proof term."Gravatar herbelin2011-12-26
* Fixed broken globalization of identifiers containing utf8 lettersGravatar herbelin2011-10-29
* Fixing bug #2606 (bad coqdoc processing of coq escaped in comments).Gravatar herbelin2011-09-22
* Fixed status of ÷ and × in coqdoc (they were seen as letter instead of symb...Gravatar herbelin2010-12-06
* Fixing several bugs with links to notation in coqdoc, including bug #2445:Gravatar herbelin2010-12-04
* Coqdoc patches from UPenn (thanks to C. Casinghino). This introduces theGravatar msozeau2010-09-28
* Fixing bug #2389 (keyword "Declare Instance" unknown from "coqdoc -g") butGravatar herbelin2010-09-19
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Applied Cédric Auger's patch to fix use of "#&xxx;" in html printingGravatar herbelin2010-04-09
* New model for user-driven translation of tokens in coqdocGravatar herbelin2010-04-06
* Small things about coqdoc + fixing lettuple.v test (part of bug #2289)Gravatar herbelin2010-03-30
* Removed hard-wiring of latin1 letters in coqdoc (see bug #2275)Gravatar herbelin2010-03-30
* Small improvements around coqdoc (including fix for bug #2288)Gravatar herbelin2010-03-30
* Fixed small bugs introduced in commit 12890 (bug #2286, that comesGravatar herbelin2010-03-30
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Adding Function as keyword for coqdocGravatar thery2010-03-06
* Fix previous commitGravatar notin2010-01-28
* Typo in previous commitGravatar notin2010-01-28
* Correction du bug #2219: application du patch envoyé par F. GarillotGravatar notin2010-01-28
* Fix make_exact_entry to allow applying [forall x, P x] hints directly,Gravatar msozeau2009-12-01
* Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les versions...Gravatar notin2009-11-12
* Misc fixes.Gravatar msozeau2009-11-06