aboutsummaryrefslogtreecommitdiff
path: root/tools
AgeCommit message (Collapse)Author
2008-06-12Correction d'un problème lié à une interaction entre hyperref etnotin
latex, qui empechait de produire des fichiers .dvi à partir des .tex générés par coqdoc. --Cette ligne, et les suivantes ci-dessous, seront ignorées-- M trunk/tools/coqdoc/coqdoc.sty M branches/v8.2/tools/coqdoc/coqdoc.sty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11120 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-11Prise en compte de l'export des .cmi dans coq_makefilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11106 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-10- Correct handling of DependentMorphism error, using tclFAIL instead ofmsozeau
letting the exception go uncatched. - Reorder definitions in Morphisms, move the PER on (R ==> R') in Morphisms where it can be declared properly. Add an instance for Equivalence => Per. - Change bug#1604 test file to the new semantics of [setoid_rewrite at] - More unicode characters parsed by coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11092 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-09Remplacement des echo -e par printf + bug sur les exécutables ocaml dans ↵notin
coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11079 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
Minor fix in Morphisms which prevented working with higher-order morphisms and PER relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11065 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Fix setoid_rewrite documentation examples.msozeau
Debug handling of identifiers in coqdoc (should work with modules and sections) and add missing macros. Move theories/Program to THEORIESVO to put the files in the standard library documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex. Next step is to test and debug it on bigger developments. On the side: - Fix Program Let which was adding a Global definition. - Correct implicits for well-founded Program Fixpoints. - Add new [Method] declaration kind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-28add support for pdf in coqdoc, add export to pdf in coqide, port open and ↵jnarboux
save as dialogs of coqide to a not deprecated widget, add filtering of *.v files in these dialogs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11006 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-29Correction d'un bug dans coq_makefile: génération des règles implicites ↵notin
en présence de l'option -custom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10869 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-08Ajout d'options a coqdoc pour l'entete htmlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10764 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-03- Correction d'un bug de coq_makefile sur les variables CAMLLIBS etnotin
COQLIBS. - Ajout d'un message d'erreur si Camlp5 est compilé en mode strict git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10746 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-26Bug dans la gestion des dépendances vers les .mlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10722 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-26Correction du bug #1814 (trunk et v8.1) + améliorations dans coqdep et ↵notin
coq_makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10721 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-25Prise en compte des dépendances des .mlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10719 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-25Correction d'un bug dans la gestion des 'Declare ML Module'notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10717 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-19Various improvements of coqdep, resulting in a big speedupletouzey
* use of Hashtbl for large sets/maps * reorganisation of directory-traversal functions, in order to avoid redundant stat / open * all files and directory whose names start by . are skipped while tranversing directories: no more visits of .svn ! * new option -boot to be used when computing dependencies of the stdlib: - no need in this case to records the system .vo in coqlibKnown - add directly inside coqdep the equivalent of -R theories Coq and -R contrib Coq As a result, coqdep'ing all the .vo of the stdlib now takes 25s on my machine instead of 2min30 earlier. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10695 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-14New option -glob for coqdep, in order to avoid nasty tricks with sed in Makefileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10668 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-08Coq_makefile : backtrack sur les liens vers les exécutables ocamlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10638 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-03-07Correction d'un bug de coq_makefilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10633 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Coq_makefile: correction de l'appel aux exécutables Ocamlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10606 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-28Coq_makefile: Correction d'un bug sur les options passées à Coqdocnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10604 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27Génération d'une toc en html et avec l'option -psnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10597 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-27Amélioration de la gestion des chemins physiques (corrige au passage le bug ↵notin
#939 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10594 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-25coq_makefile: variablesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10586 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-25coq_makefile: dépendances + génération des fichiers htmlnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10585 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-25Bug de coqdoc : les commentaires simples généraient des lignes videsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10584 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-25Correction d'un bug de Coqdoc (indentation des lignes)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10583 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Bug de Coqdoc avec l'option -Rnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10569 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-14Reconnaissance des tokens dans les notations (suite à la revision r10562)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10567 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Correction du bug #1512notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10562 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-13Suppression de l'option -glob-from de Coqdoc: les globalisations sontnotin
lues directement des fichiers .glob git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10559 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Oubli dans r10524notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10525 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-02-08Correction d'un bug de Coqdoc + ajout de Include dans les mots clés ↵notin
reconnus par Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10524 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-01-30Add some keywordmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10480 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-31Merged revisions ↵msozeau
10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-18Petite correction sur coq_makefilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10391 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-12-17Correction d'un bug dans Coqdoc: les mots clés liés aux sections étaient ↵notin
supprimés par l'option -g git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10386 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-23Ajout de mots clés pour Coqdoc (bug #1732)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10248 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-22Corrections des bugs #1730 et #1731notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10246 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-17Prise en compte des .glob par coq_makefilenotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10231 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-10-08Calcul des dependances sous Windowsnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10196 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-08-13Correction (partielle) bug #1052 (coqdoc supprime les fins de ligne après ↵notin
un commentaire) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10074 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-06-21Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, notin
et une typo dans Eqdep_deq.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9905 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-16- MAJ entêtes des fichiers produits par coq_makefileherbelin
- Correction de bugs dans la reconnaissance d'un "*)" potentiel dans les lignes correspondant au mécanisme "section" de coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9826 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-05-07Correction du bug #1509notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9818 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-04-23Correction du bug #1496 (ajout de Program Definition et Program Fixpoint aux ↵notin
commandes vernac considérées par Coqdoc) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9790 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-22Correction des bugs #1455 et #1456notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9728 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-22Remove debugging code committed by accidentlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9727 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-03-22A tentative fix for bug #1455lmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9726 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 09:08:07 +0000