aboutsummaryrefslogtreecommitdiff
path: root/tools
AgeCommit message (Collapse)Author
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
2007-03-08Add Program keywords to coqwcmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9691 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-24Améliorations utiles pour les Makefile répartis sur plusieurs répertoiresherbelin
coqdep : - fonction de "canonisation" du nom des cibles plus performante (elle traverse notamment les "..") coq_makefile : - ajout automatique de "-I ." dans COQLIBS seulement si pas déjà déclaré (utile pour éviter les cibles en double dans coqdep en présence de -R) - explicitation de "-byte" dans la cible "byte:" (son absence semble remonter à l'époque où l'exécution en byte était le défaut) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9676 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-16Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9656 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-16Missing keywordmsozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9654 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-02-11Add keywords that were missing, notably for terms.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9638 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-29Coqdoc patch for Program, fix xlate.ml warning and little subtac fixes.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9550 85f007b7-540e-0410-9357-904b9bb8a0f7
2007-01-24doc de ringbgregoir
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9532 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-25coqdep -slashbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9276 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-17Mise en forme des theoriesnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9245 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-10-04Correction bug #1204 + maj CHANGESnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9204 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-08Warning ocaml 3.09 pour variable inutileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8923 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-26Support des modules dans Coqdocnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8863 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-24Adaptation de Coqdoc au nouveau add_globnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8861 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-22Modification de l'appel à coqdoc (COQBIN)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8840 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-02Option --coqlib_path pour coqdoc (suite et fin)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8777 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-05-02Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. ↵notin
Mimram) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8775 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8762 ↵notin
85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-28Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des ↵notin
'properties' de Subversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8758 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-27Ajout de la doc de l'option -stdout de coqdocnotin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8749 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8742 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Outil de test de la réversibilité du réafficheur v8->v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8740 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Prise en compte du Require multipleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8737 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-26Correction d'un bug dans coqdoc sur l'utilisation de l'option -o et la ↵notin
création du fichier de style git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8734 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-28- correction d'un bug dans coqdoc (multi_index)notin
- 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
2006-03-27Correction d'un bug dans Coqdoc (indentation & mots clés)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8666 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-25 r8709@thot: notin | 2006-03-25 01:48:46 +0100notin
- Ajout de FSets dans la doc de stdlib - coqdoc copie la feuille de style dans le répertoire courant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8663 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-25 r8686@thot: notin | 2006-03-20 19:29:09 +0100notin
Correction d'un bug dans Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8661 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-17Modification des propriétés (svn:executable)notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8642 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-14 r8636@thot: notin | 2006-03-14 15:57:11 +0100notin
Correction de bugs de Coqdoc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8625 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-03-08 r8620@thot: notin | 2006-03-08 11:44:16 +0100notin
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
2006-02-06Ajout de l'essai d'effacement des noms des cibles custom par la cible cleanherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7994 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-11Suppression traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7846 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-01-06Petite modification de la gestion du '.' (jmn)coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7807 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 18:12:56 +0000