| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
This does not affect the rendering but gives better structured
html/tex files.
|
|
We clarify that there are two kinds of verbatim: inline and block.
We add a test testing verbatim and others.
Co-authored-by: Xia Li-yao <Lysxia@users.noreply.github.com>
|
|
|
|
This is to avoid collision with the syntax of the host output language.
|
|
|
|
Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>
|
|
This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.
In particular, this fixes #7697.
|
|
Reviewed-by: Lysxia
Reviewed-by: Zimmi48
|
|
|
|
We propose to add an environment to have foldable texts with HTML
output, more precisely:
(*begin details [: An optional summary] *)
some Coq and documentation material
(* end details *)
Currently, only the HTML output is supported. We could treat this
environment in LaTeX output as appendixes to output later.
|
|
Add headers to a few files which were missing them.
|
|
Fixes #10576
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
|
|
The changes are large due to `Pervasives` deprecation:
- the `Pervasives` module has been deprecated in favor of `Stdlib`, we
have opted for introducing a few wrapping functions in `Util` and
just unqualified the rest of occurrences. We avoid the shims as in
the previous attempt.
- a bug regarding partial application have been fixed.
- some formatting functions have been deprecated, but previous
versions don't include a replacement, thus the warning has been
disabled.
We may want to clean up things a bit more, in particular
w.r.t. modules once we can move to OCaml 4.07 as the minimum required
version.
Note that there is a clash between 4.08.0 modules `Option` and `Int`
and Coq's ones. It is not clear if we should resolve that clash or
not, see PR #10469 for more discussion.
On the good side, OCaml 4.08.0 does provide a few interesting
functionalities, including nice new warnings useful for devs.
|
|
|
|
|
|
|
|
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
|
|
|
|
As stated in the manual, the fourier tactic is subsumed by lra.
|
|
Unused since 6832c60f741e6bfb2a850d567fd6a1dff7059393.
|
|
|
|
Fix proposed by the reporter, Vincent Laporte.
Note that for LaTeX output, the selection of a keyword was already
done after checking if the ident is recognized as a Coq ident by
coqtop.
Incidentally, being now explicit on an wildcard-catching of exceptions.
|
|
|
|
|
|
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]
|
|
|
|
|
|
|
|
(thanks to coq-club, Sep 2015).
|
|
|
|
|
|
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 />
|
|
documentation en ligne)
|
|
|
|
Just like the [Record] keyword allows only non-recursive records.
|
|
|
|
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.
|
|
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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
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
|
|
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
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
