aboutsummaryrefslogtreecommitdiff
path: root/tools/coqdoc
AgeCommit message (Collapse)Author
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-23Support "Functional Scheme" in coqdoc. (Fix bug #4382)Guillaume Melquiond
2015-09-26Documenting how to support some special unicode characters in coqdocHugo Herbelin
(thanks to coq-club, Sep 2015).
2015-09-26Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.Hugo Herbelin
2015-07-30Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.Guillaume Melquiond
"This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code."
2015-04-02Avoid outputting stray "Local" keywords in HTML documentation.Guillaume Melquiond
2015-03-31Do not escape "'" when outputting to html, especially not using "´".Guillaume Melquiond
2015-02-11Make coqdoc -l properly handle Local before Ltac. (Fix for bug #3307)Guillaume Melquiond
2015-01-12Update headers.Maxime Dénès
2015-01-06Improve error recovery in case of ill-formed coqdoc comment. (Fix for bug ↵Guillaume Melquiond
#3802.)
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-12-09coqdoc.css: fix a few errorsPierre Letouzey
2014-12-09coqdoc: fix a few issues with xhtml validity (backport 1636f7 and 754abf1 ↵Pierre Letouzey
from v8.4) - For the style of identifiers, coqdoc was using a 'type' attribute of tag <span>. But this attribute isn't a legal attribute of tag <span> according to the xhtml norm. Instead, I propose to use 'title' for that. The coqdoc.css now supports both approaches. - The names of inner links (cross references #foo) were containing arbitrary characters (in the case of a notation string). For instance in Utf8_core : <a name=":type_scope:'∀'_x_'..'_x_','_x"> Instead, when strange characters are detected, we now hash the string via Digest, and use this hexa hash as html label. - And some whitespace before />
2014-12-09Port to trunk commit r16062 of v8.4 (Correction des entêtes pour la ↵notin
documentation en ligne)
2014-10-27Use the url package, since coqdoc generates \url commands.Guillaume Melquiond
2014-10-22Supporting Greek and Coptic (U0370) as first letter of coqdoc identifiers.Hugo Herbelin
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
Involves changing the [mind_finite] field in the kernel from a bool to the trivalued type [Decl_kinds.recursivity_kind]. This is why so many files are (unfortunately) affected. It would not be very surprising if some bug was introduced.
2014-09-04Add a [Variant] declaration which allows to write non-recursive variant types.Arnaud Spiwack
Just like the [Record] keyword allows only non-recursive records.
2014-07-03coqdoc is minimaly -Q awarePierre Boutillier
2014-04-28Recognize Parameters as a command in coqdoc. (Fix for bug #3279)Guillaume Melquiond
2014-04-28Mark lazymatch as an Ltac keyword for coqdoc. (Fix for bug #3276)Guillaume Melquiond
2014-04-28Fixing coqdoc bug #3292 (unfortunate collision betweens the relativeHugo Herbelin
locations found when parsing expressions in comments and the absolute locations in the glob file). As now, the glob file does not parse comment, so I removed the test for location when parsing expressions in comments, which anyway are not linkable, precisely because not parsed by coqc.
2014-04-10Dumpglob: factor out reference dumping.Carst Tankink
Factored out all functions that dump references to use one function "dump_ref"
2014-04-04Prevent verbatim text from leaking out of comments. (See bug #2882)Guillaume Melquiond
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2014-03-02Set officially the minimal OCaml requirement to 3.12.1Pierre Letouzey
Anyway, a few syntactic features of 3.12 were already used here and there (e.g. local opening via Foo.(...), or the record shortcut { field; ... }). Hence compiling with 3.11 wasn't working anymore. Already take advantage of the following 3.12.1 features : - "module type of ..." in CArray, CList, CString ... - "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output via our coqdep to localize the .ml4 modules :-) The -ml-synonym option (+ various bugfixes) is the reason for asking 3.12.1 directly and not just 3.12.0. After all, if debian stable is providing 3.12.1, then everybody has it ;-)
2013-10-14Avoid polymorphic comparison (coqdoc).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16884 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-10-14Getting rid of the use of deprecated elements (from the OCaml standard library).xclerc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-22Misc changes around coqtop.ml :letouzey
- Revised Coqtop.parse_args in a cleaner and lighter style - Improved error message in case of argument parse failure: * tell which option is expecting a related argument * in case of unknown options, warn about them all at once * do not hide the previous error messages by filling the screen with usage(). Instead, suggest the use of --help. - Specialized boolean config field Coq_config.arch_is_win32 - Faster Envars.coqlib, which is back to (unit->string), and just access Flags.coqlib. Caveat: it must be initialized once via Envars.set_coqlib - Avoid keeping an opened channel to the "revision" file - Direct load of theories/init/prelude.vo, no detour via Loadpath Beware : ./configure must be runned after this commit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-17Renaming SearchAbout into Search and Search into SearchHead.herbelin
I hope I did not forget any place to change. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16270 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Continuing r15885 fixing coqdoc index bugs introduced in r14624 and r15053.herbelin
Indeed r15885 still had problems (index contained referenced objects and not only defined objects, sorry). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15893 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-16Removed dead code about linking Module names in coqdoc.herbelin
Code was probably unused since scan_file made obsolete in r11024. See also r12890. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15892 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-15Fixing coqdoc index bugs introduced in r14624 and r15053. Revision r14624 ↵pboutill
introduced bug #2709 on duplicate entries in index and tentative fix of it in r15053 mixed up names of files and names of constants in index (as reported by P. Castéran on coqdev). Patch by Hugo Herbelin :-) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15885 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06still some more dead code removalletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
especially about unused definitions, unused opens and unused rec flags. The following patch uses information gathered using these warnings to clean Coq source tree. In this patch, I focused on warnings whose fix are very unlikely to introduce bugs. (a) "unused rec flags". They cannot change the semantics of the program but only allow the inliner to do a better job. (b) "unused type definitions". I only removed type definitions that were given to functors that do not require them. Some type definitions were used as documentation to obtain better error messages, but were not ascribed to any definition. I superficially mentioned them in one arbitrary chosen definition to remove the warning. This is unaesthetic but I did not find a better way. (c) "unused for loop index". The following idiom of imperative programming is used at several places: "for i = 1 to n do that_side_effect () done". I replaced "i" with "_i" to remove the warning... but, there is a combinator named "Util.repeat" that would only cost us a function call while improving readibility. Should'nt we use it? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-09-07Coqdoc: fix --utf8 bug for pretty printingpboutill
Author: Francois Ripault <francois.ripault@epita.fr> git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15782 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
For starting a bare coqtop, the recommended option is now "-noinit" that skips the load of Prelude.vo. Option "-nois" is kept for compatibility, it is now an alias to "-noinit". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15753 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Coqdoc inlined verbatim_char in latexpboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15690 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-06Add inline verbatim (<</>>), quotes (") and urls ({{url} name}) ↵pboutill
markup/typesetting to coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15689 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05Coqdoc: More keywords, better special char escape, special case for "in *"pboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15680 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-05More entries in the indexpboutill
Patch by Adam Chilipala. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15678 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-07-18Various minor fixes to coqdoc from A. Chlipala.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15624 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-19Bug 2709: Duplication in coqdoc index entriespboutill
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15053 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-02-16Fix handling of space after "Notation" or "where", add missing keywords.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14983 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-26Coqdoc: Fixing missing newline when using "Proof term."herbelin
(bug apparently introduced by r11880). Fixing also a "body_bol" which apparently should be a "bol". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14866 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-29Fixed broken globalization of identifiers containing utf8 lettersherbelin
without knowing it. Note: location tables have grown a lot, a better representation of the contents of the glob files in coqdoc might improve efficiency. Also added keywords. Information is now obtained from the glob file to know the exact span of identifiers. Kept a class of identifiers (and enriched them) for the main purpose of distinguishing between idents and symbols in the absence of a glob file. Still a lot of work to do in coqdoc to make it more robust... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14624 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-10-29Added checksums to glob files and warned about possibly missingherbelin
packages for utf8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 22:12:28 +0000