| Age | Commit message (Collapse) | Author |
|---|
|
- Correct backtracking function of coqdoc to handle the _p fields of lexers
- Try a better typesetting of [[ ]] inline code considering it as
blocks and not purely inline code like [ ] escapings.
- Rework latex macros for better factorization and support external
references in pdf output.
- Better criterion for generalization of variables in dependent
elimination tactic and better error message in [specialize_hypothesis].
- In autounfold, don't put the core unfolds by default.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
by Chris Casinghino).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12311 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
M. Greenberg) and add support for interpolation to HTML output. The
patch is mostly backwards-compatible, except for the CSS style which
needs more readaptation. Doc for the new options will come as well.
- lists have been updated substantially. In particular,
multiparagraph list items are now supported and sublists work
better, using an "off-side" rule.
- the "--index" flag allows one to change the name of the generated
index file (good since index.html has a special meaning).
- the "--toc-depth <int>" flag allows one to limit how many levels are
included in the toc.
- the "--lib-name <string>" flag allows one to specify what libraries
are called, instead of just sticking "Library" before each module
name (for example, "Module" or "Chapter" might be more sensible in
some contexts). Additionally "--no-lib-name" eliminates this extra
title completely.
- the "--lib-subtitles" flag allows one to specify subtitles for
libraries. When enabled, the beginning of each file is checked
for a comment of the form:
(** * ModuleName : text *)
and the text will be printed as a subtitle in the appropriate
places.
- Text can be made italic by putting it inside underscores, as in:
_emphasized text_. This has the advantage of looking OK in the
.v file as well. A few simple rules are followed to make sure
identifiers with underscores aren't accidentally made italic.
- Various changes have been made in an attempt to beautify the output,
especially in html, while allowing the .v sources to look decent as
well. Mostly these involve whitespace.
- The coqdoc.css file has been changed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12308 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
B. Pierce on coq-club).
- Output regular comments, enclosed in a span in HTML (with (* *)
delimiters) and inside a new environment in LaTeX.
- HTML output: put the span inside anchors in links, so as to keep the
same style as for definitions (customizable in the CSS).
- Better handling of Next Obligation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12004 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Better handling of spaces by actually ignoring what's inside proof
scripts in light/gallina mode (detection of [Proof with] vs [Proof.] vs
[Proof t.] and [Qed]/[Save]/...).
- Provide fancy replacements for forall,/\,... etc in HTML in case the
utf8 option is on.
- Use typesetting information in HTML output and customize the CSS
accordingly. The default color scheme follows closely the one set by
Conor for Epigram; of course one can change it.
- A try at interpolating identifiers in comments if they are defined in
the same module, with a corresponding flag.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11421 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- modif. de la génération de la doc de stdlib
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8669 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Modifications diverses de Coqdoc:
- modification du comportement par défaut de l'option --latex
- ajout d'une option --stdout
- réaménagement dans les sources (création de global.ml)
- modification du parser de coqdoc pour regler les problèmes liés à
la syntaxe V8.
- Correction du bug #1052 sur les commentaires en fin de ligne
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8617 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(i.e. the output is no longer HTML but (X)HTML)
2. Added (** ^ ... ^ *) to output verbatim characters that are NOT
quoted (whereas (** # ... # *) and all the other similar marks
do quote the characters according to the output language quoting
conventions).
3. Added ^^ to output a single '^' character
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5647 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5580 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5377 85f007b7-540e-0410-9357-904b9bb8a0f7
|
