aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-03-29eq fusionne avec eqT et devient par défaut sur Type,herbelin
idem pour ex et exT, ex2 et exT2, all et allT git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3812 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29indentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3811 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Déplacement de minus dans Peanoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3810 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Implicit Variables Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3809 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Implicit Variables Type dans les inductiveherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3808 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3807 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3806 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3805 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28coqide: command window maj.monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3804 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28Pas d'associativité gauche au niveau 3 en vieille syntaxe !herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3803 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28notations <>, Assumption avec existentiel, replace termmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3802 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28coqide: bug undo corrigemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3801 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28Réparation bug de l'unification. En effet, avant l'instanciation d'une evarclrenard
on n'unifiait pas les types ce qui est maintenant fait. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3800 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-28Fixed Relative names not,iff in Camlp4 quotation.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3799 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-27coqide: bugfix du C-C pendant Undo+paren_highlightmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3798 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-27MAJ des mots-clés, Definition, Theorem, ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3797 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-27MAJ des mots-clés, Definition, Theorem, ...herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3796 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-27coqide: efficacite des buts etc...monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3795 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-27Affinement nommage des productionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3794 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-26coqide: locale iso-8859-1 par defaut si probleme. Interdiction des lemmes ↵monate
locaux. Reparation du Undo avec Section et constantes de meme nom. Decoupe tag modifie git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3793 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-26coqide: addloadpath corrigemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3792 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-26ajout d'une fonction reset_modmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3791 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-26Ajout de Set Print Widthgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3790 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3789 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-25Extract Constant marche avec les axiomes schémas de typesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3788 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-24coqide: compact delete event-search startmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3787 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-24pour faire marcher le control-kletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3786 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-24Bugfix pour Linear.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3785 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3784 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3783 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21correction affichage des modulesbarras
amelioration des commentaires preservation des locations de constrextern (en vue d'un affichage des commentaires a l'interieur d'une commande vernac). meilleure traduction automatique des niveaux git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3782 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-21Fin de la résurrection de Linear.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3781 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-18Introducing Christine's Intuition1 and adding some invertible hyps.corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3780 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-18Ajout translateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3779 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-17coqmktop: -ide fait ce qu'il faut (on peut maintenant construire des Coq IDE ↵filliatr
customises) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3778 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-17nettoyage dans translatefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3777 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3776 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-15petit oubliletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3775 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14coqide: maj preferences du wizzardmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3774 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14coqide: utf8.vmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3773 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14nettoyage dans ide/utilsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3772 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3771 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3770 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14reparations suite a la nouvelle syntaxe:barras
- syntaxe des modules - syntaxe existentielle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3769 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14notations coqidemonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3768 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14*** empty log message ***monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3767 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-14coqide: maj commandesmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3766 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-13Ajout réaffichage SubClassherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3765 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-13code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3764 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3763 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 09:54:54 +0000