aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/alpha.ml
Commit message (Collapse)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Fail on deprecated warning even for Ocaml > 4.02.3Gravatar Gaëtan Gilbert2017-05-28
| | | | | | | | Deprecations which can't be fixed in 4.02.3 are locally wrapped with [@@@ocaml.warning "-3"]. The only ones encountered are - capitalize to capitalize_ascii and variants. Changing to ascii would break coqdoc -latin1 and maybe other things though. - external "noalloc" to external [@@noalloc]
* [safe-string] toolsGravatar Emilio Jesus Gallego Arias2017-03-14
| | | | No functional changes.
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - make links to section variables working (used qualified names for disambiguation and fixed the place in intern_var where to dump them) (wish #2277) - mapping of physical to logical paths now follows coq (see bug #2274) (incidentally, it was also incorrectly seeing foobar.v as a in directory foo) - added links for notations - added new category "other" for indexing entries not starting with latin letter (e.g. notations or non-latin identifiers which was otherwise broken) - protected non-notation strings (from String.v) from utf8 symbol interpretation - incidentally quoted parseable _ in notations to avoid confusion with placeholder in the "_ + _" form of notation - improved several "Sys_error" error messages - fixed old bug about second dot of ".." being interpreted as regular dot - removed obsolete lexer in index.mll (and renamed index.mll to index.ml) - added a test-suite file for testing various features of coqdoc Things that still do not work: - when a notation is redefined several times in the same scope, only the link to the first definition works - if chars and symbols are not separated in advance, idents that immediately follow symbols are not detected (e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}") - parentheses, curly brackets and semi-colon not linked in notations Things that can probably be improved: - all notations are indexed in the same category "other"; can we do better? - all non-latin identifiers (e.g. Greek letters) are also indexed in the same "other" category; can we do better? - globalization data for notations could be compacted (currently there is one line per each proper location covered by the notation) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdocGravatar filliatr2004-02-24
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5377 85f007b7-540e-0410-9357-904b9bb8a0f7