aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
Commit message (Collapse)AuthorAge
...
* Fix make_exact_entry to allow applying [forall x, P x] hints directly,Gravatar msozeau2009-12-01
| | | | | | | | | avoiding the introduction of eta-redexes. Prioritize hints over intros in typeclass resolution to profit from that. Add a minor fix in coqdoc by F. Garillot. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12550 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les ↵Gravatar notin2009-11-12
| | | | | | versions de OCaml antérieures à 3.11.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12512 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #2183Gravatar notin2009-11-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12492 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc fixes.Gravatar msozeau2009-11-06
| | | | | | | | | | | | | | - 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
* Removed debugging stuff mistakenly introduced in r12426.Gravatar herbelin2009-11-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12465 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed 'dest' from keyword highlighting.Gravatar gmelquio2009-10-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrate a few improvements on typeclasses and Program from the equations ↵Gravatar msozeau2009-10-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Added option --external to coqdoc to bind an url to an external library.Gravatar herbelin2009-10-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better handling of emphasis.Gravatar msozeau2009-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12385 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
* - Tentatively made order-dependency wrt .vo files a full dependencyGravatar herbelin2009-09-15
| | | | | | | | | | | of the doc (use "make QUICK=1" to shortcut it) otherwise, the compilation of the doc is re-checked only when the doc files are removed. - Fixed a typo in coqdoc.sty and a redundancy in Makefile.common . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12334 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for toc depth handling and handling of substitles from Chris Casinghino.Gravatar msozeau2009-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12318 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update coqdoc documentation, CHANGES and add a fix for the proofbox (patchGravatar msozeau2009-09-08
| | | | | | | by Chris Casinghino). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
| | | | | | | | | | | | | | | | | | | rewriting (thanks to Georges Gonthier for pointing it out). We try to find a declared rewrite relation when the equation does not look like an equality and otherwise try to reduce it to find a leibniz equality but don't backtrack on generalized rewriting if this fails. This new behavior make two fsets scripts fail as they are trying to use an underlying leibniz equality for a declared rewrite relation, a [red] fixes it. Do some renaming from "setoid" to "rewrite". Fix [is_applied_rewrite_relation]'s bad handling of evars and the environment. Fix some [dual] hints in RelationClasses.v and assert that any declared [Equivalence] can be considered a [RewriteRelation]. Fix minor tex output problem in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Incorporate coqdoc changes by the UPenn team (B.Pierce, C. Casinghino,Gravatar msozeau2009-09-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Add --plain-comments patch by F. Garillot, which also addsGravatar msozeau2009-09-03
| | | | | | | | | 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
* Allow coqdoc comments inside definition bodies.Gravatar msozeau2009-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12237 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report de la révision #12104 (Maj lien site web de Coq)Gravatar notin2009-04-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12105 85f007b7-540e-0410-9357-904b9bb8a0f7
* Take formatted into account in rules for dot.Gravatar msozeau2009-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12072 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change HTML paragraph output to avoid too much space after bulletedGravatar msozeau2009-04-08
| | | | | | | lists, patch by B. Pierce. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12067 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix behavior on newlines with parse-comments and also do [] escaping as Gravatar msozeau2009-04-06
| | | | | | | 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
* Protect typeset arguments in titles in LaTeX output (fixes compilationGravatar msozeau2009-03-26
| | | | | | | errors in Library.coqdoc). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12017 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix coqdoc bugs reported by Ian Lynagh.Gravatar msozeau2009-03-24
| | | | | | | | - 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
* pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5 file)Gravatar letouzey2009-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 85f007b7-540e-0410-9357-904b9bb8a0f7
* More elaborate handling of newlines in Gallina mode. Support inlineGravatar msozeau2009-03-22
| | | | | | | Qed's. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12005 85f007b7-540e-0410-9357-904b9bb8a0f7
* coqdoc fixes and support for parsing regular comments (request byGravatar msozeau2009-03-22
| | | | | | | | | | | | 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
* Report des revisions #11826, #11828 et #11829 de v8.2 vers trunkGravatar notin2009-02-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11915 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix d'un bug avec l'option gallinaGravatar notin2009-02-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11880 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Better deal with commands inside section titles in latex output usingGravatar msozeau2009-01-21
| | | | | | | | the support from hyperref. - Rename n-ary 'exist' tactic to 'exists' in Program.Syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various little fixes:Gravatar msozeau2009-01-18
| | | | | | | | | | | | - allow a new line after a (** printing *) directive in coqdoc so as not to output spurious new lines. - never directly unify the lemma with an evar in setoid_rewrite (they act as opaque constants). - Fix a useless dependency introduced by tauto which splits a record in SetoidList. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11799 85f007b7-540e-0410-9357-904b9bb8a0f7
* Patch by Brian Campbell to output more information on the exception thatGravatar msozeau2009-01-15
| | | | | | | made a glob file unreadable. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11788 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor doc fixes:Gravatar msozeau2009-01-08
| | | | | | | | | | | - Set BIBINPUTS variable correctly so that we do not use any random biblio.bib file. - Update setoid_rewrite doc to new typeclasses syntax and fix verb -> texttt - Stop using less than 100% line heights in coqdoc.css git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite de la révision #11756Gravatar notin2009-01-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11757 85f007b7-540e-0410-9357-904b9bb8a0f7
* Produce better html code with coqdoc and improve doc:Gravatar msozeau2008-12-29
| | | | | | | | | | - correct nesting of a and div (fixes bug #2022) - use span instead of div for inline parts - fix standard lib template missing/new links - use -g to produce the stdlib doc (no proofs) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des variables Coq et amélioration de coqmktop. LesGravatar notin2008-12-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | principaux changements sont: - coqtop (et coqc) maintenant insensible aux variables d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les librairies Coq peut être spécifié par l'option -coqlib - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les chemins des exécutables OCaml; en dehors du mode boot, coqmktop cherche les exécutables OCaml dans PATH - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci étant installé en copiant l'architecture des sources (ie lib.cmxa est installé dans COQLIB/lib/lib.cmxa) - coq_makefile prend maintenant 3 paramètres sous forme de variables d'environnement: COQBIN pour dire où trouver les exécutables Coq, CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les chemins vers les librairies sont déduits en utilisant -where Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de simuler les conditions de la vie réelle (Ocaml pas dans le PATH, installation binaire relocalisée, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration du README.doc et de l'installation de la docGravatar notin2008-11-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes:Gravatar msozeau2008-11-05
| | | | | | | | | - Rework definition of the type of respecful functions in Morphisms.v - Unfold [flip] in "Add Morphism" tactic (suggested by N. Tabareau) - Add a "coqvariableref" command in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'une option -raw pour Coqdoc (sortie en texte brut)Gravatar notin2008-10-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11529 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stop using a coqdocdoc env which prevents use of environments insideGravatar msozeau2008-10-26
| | | | | | | | | comments that go across code and doc (e.g. for beamer frames), it was unused anyway. Add "do" and "repeat" as tactic identifiers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11507 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various coqdoc improvements:Gravatar msozeau2008-10-22
| | | | | | | | | | | | | - New "color" option to the coqdoc latex style file to typeset using the xcolor package, still following the McBride convention. - Work on proper indentation and spacing of output code and allow users to customise indentation (setting a base indentation length) and line skips for empty lines of code. - Also add new environments to distinguish code and documentation, doing nothing right now. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11491 85f007b7-540e-0410-9357-904b9bb8a0f7
* ## Lines starting with '## ' will be removed from the log message.Gravatar msozeau2008-10-06
| | | | | | | | | | | | | | | | ## File(s) to commit: ## tools/coqdoc/index.mll ## tools/coqdoc/output.ml ## tools/coqdoc/pretty.mll Various improvements to coqdoc: - (Hopefully) better handling of brackets and notations like \in (debugger with Stéphane Lescuyer). - More indexed tactics and commands. - Fix bug(?) in parsing of "[[" comments. - Better interpolation of module and library names. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11432 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes related to coqdoc and --interpolate and the dependentGravatar msozeau2008-10-03
| | | | | | | induction test-suite script. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11426 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot one file.Gravatar msozeau2008-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11422 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in coqdoc:Gravatar msozeau2008-09-25
| | | | | | | | | | | | | | | | - 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
* Add types introduced by subtac in *.glob filesGravatar glondu2008-09-15
| | | | | | Hints from compilation warnings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11412 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1908 (améliorations de coqdoc.css)Gravatar notin2008-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11361 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from ↵Gravatar notin2008-07-18
| | | | | | de coqdoc (compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11236 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coqdoc: correction d'un bug sur les commentaires imbriquésGravatar notin2008-07-17
| | | | | | | | - coq_makefile: amélioration des chemins de camlp4/5 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11231 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli lors de la révision #11177Gravatar notin2008-06-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11179 85f007b7-540e-0410-9357-904b9bb8a0f7
* Création du fichier dumpglob.ml, qui rassemble les fonctions de ↵Gravatar notin2008-06-25
| | | | | | globalisation (add_glob* et dump_*) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11177 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 00:53:04 +0000