aboutsummaryrefslogtreecommitdiff
path: root/theories7/Init
AgeCommit message (Collapse)Author
2005-12-26Suppression des fichiers .v en ancienne syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7733 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Tactics.v bidon pour accomoder make world7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6671 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 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-03-17Definition de la notation de la paire par un motif recursifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5519 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-12Bug compatibiliteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5465 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-28MAJ Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5397 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-02-12Décomposition automatique des règles d'analyse syntaxique pour lesherbelin
notations contenant le motif "{ _ }": permet de réperer des incohérences de précédence comme dans "A*{B}+{C}" en présence d'une notation "_ * { _ }" (il était parsé associant à droite au lieu de à gauche) et de supprimer les règles spécifiques de Notations pour parser "B+{x:A|P}" etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5319 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-07Vieille syntaxeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5183 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-23Finalement, espacement autour du ':' pour a la fois exists, forall et funherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5135 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-21Affichage sur le modèle du forall pour le existsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5125 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16exists | --> exists ,barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5103 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-16Duplication temporaire des règles de syntaxe des pairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5102 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-05power associe a droitemarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5072 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5030 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-29Deplacement des fichiers ancienne syntaxe dans theories7, contrib7 et states7herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5026 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-16 23:43:05 +0000