aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-04-27Correction incapacité à gérer les annotations de type dépendantes pour ↵herbelin
le if-then-else git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5706 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5702 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5701 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5700 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5699 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5698 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5696 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-21pb install de pcoqbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5695 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5694 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5693 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20amelioration des specs RPMbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5692 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20Amélioration message d'erreur quand échec unificationclrenard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5691 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-20maj annonce depuis la v8beta vers v8narboux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5690 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5689 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-18majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5688 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17Incorrection exportation XMLherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5687 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17Finalement pas de liste des contributions (cela n'avait été fait que pour ↵herbelin
la 7.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5686 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17pb facto des Fixpoint + erreur avec -dump-glob et Loadbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5684 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-16Backtrack user contribsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5683 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-16Nouvelles majsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5682 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-16Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5681 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-16MAJ setupherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5680 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5679 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-15Bug réaffichage EXTherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5678 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-15MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5677 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5676 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5675 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-14MAJ numéro magiqueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5674 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-14Ajout exemple Brunoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5673 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5672 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-13Ajout codingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5671 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-13Passage a la version 1.3 sous GPL des outils okey et configwin de cameleon ↵herbelin
en remplacement de la version 1.2 qui etait sous QPL git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5670 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-13Suppression documentation option raw-comments qui est vraiment trop ad hoc ↵herbelin
pour l'export XML des .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5669 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-13Correction confusion entre la dependance en les termes filtrees dans ↵herbelin
l'annotation donnee par l'utilisateur et l'annotation utilisee en interne git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5668 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5667 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-11majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5666 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5665 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5664 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-08Chgt role 2eme argument AList et implantation affichage motifs recursifs de ↵herbelin
notations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5663 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-08Incoherence bytecamlc et camlc si echec a trouver ocamlc.opt avec option ↵herbelin
-opt (cd discussion bug #611) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5662 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Copyright notice of files in contrib/xml made uniform.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5661 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5660 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5659 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Old file. The new version of this script is no longer distributed withsacerdot
Coq (the latest verion can be retrieved from the HELM and MoWGLI pages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5658 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07- theoryobject.dtd is the DTD for .theory filessacerdot
- copyright notice inserted in every DTD git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5657 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07Loic code to pretty-print the generated proof-tree debranched (since itsacerdot
generates not well-formed XML files). An hook is left in xmlcommand.ml to register a pretty-printer function once a fixed implementation is provided. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5656 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07preparation a la release 8.0barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5655 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5654 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-07bug #606: mis un message d'erreur plus clairbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5653 85f007b7-540e-0410-9357-904b9bb8a0f7