| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
branch
and remove equations stuff which moves to a separate plugin.
Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when
they are changed by a [Hint Extern] in typeclass resolution.
Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
and produce the smallest proof terms possible.
Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with
[generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
(might introduce a few changes in the contribs).
Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations,
automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for
every defined obligation constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12385 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12318 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
|
| |
|
|
|
|
|
|
|
| |
interpretation of [[ etc... inside (* *) comments when --parse-comments
is used. Add some additional fixes from B. Pierce on formatting
verbatim and the HTML Toc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12307 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12237 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
usual in this mode (report and request by B. Pierce).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12054 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
- Add coqdoccomment LaTeX environment to sty file
- Fix buggy parsing in comments
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12013 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 85f007b7-540e-0410-9357-904b9bb8a0f7
|
msozeau
glondu
letouzey