aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-03-31Noms absolusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3829 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout double_plusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3828 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout Implicit Variable Typeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3827 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Plus de eqT; message Failherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3826 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTacherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un message à FailTac; localisation des appels à des tactiques ↵herbelin
définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3824 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Mise en place d'un traducteur de noms v7->v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3823 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout d'un choix 'onlyparse'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3822 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Suppression des alias eqT/exT/exT2 en nouvelle syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3821 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Ajout VernacReserve et suppression des types re-inferablesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3820 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Restauration de make_all_different (disparu depuis version 1.74) car sinon ↵herbelin
detype echoue sur les variables anonymes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3819 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Bug pattern_occ_hyp_listherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3818 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Correcting a bug occuring when the mimicked function had acourtieu
lambda-abstraction inside a Cases. I had to make the term of the induction principle a bit less clean (more eta expansions). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3817 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31Notation eqT superflueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3816 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31minus a changé d'emplacement -> omega pas contentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3814 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3813 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 01:14:47 +0000