aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-01-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5214 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5213 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-16ajoute une option -linkall dans compilation de bin/parser pour assurer quebertot
les analyseurs syntaxiques sont bien charges git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5212 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-16Corrige: Intros [] etait traduit intros (), qui ne reparse pasbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5211 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5210 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-15translation to structures now okay for pattern matching constructsbertot
The locations in simpl, unfold, and the like are also better taken into account git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5209 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-15Ajout nouvelles optionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5208 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-15Ajout load-vernac-source-verboseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5207 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5206 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5205 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-14compact nested universal quantifications into a single quantification withbertot
a list of binders git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5204 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-14make sure the parser for FORMULA does not require them to be enclosed inbertot
parentheses and parse to the end of input git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5203 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-14Now, the grammar extension from .v files are concentrated in just a fewbertot
files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5202 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-14make libraries, lexing of more utf8 symbolsmarche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5201 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5200 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5199 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables ↵herbelin
a b:A' et 'Variables (a:A) (b:A)' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5198 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13Suppression de Rsyntax en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5197 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13Reference obsolete au niveau 200 de patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5196 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5195 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-12Set is not always impredicativebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5194 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5193 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5192 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5191 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-09bugs avec Pose et Assertbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-09Commentaires en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5189 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-09Retrait de la notation '^' pour 'power' en V7 car sinon confusion avec la ↵herbelin
syntaxe '^' de append qui est a un autre niveau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5188 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5187 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-08Finalisation du mecanisme de creation du rpm coqideherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5186 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-08Ajout cible install-ideherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5185 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5184 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
2004-01-07Cible redondante qui trouble les make non linuxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5182 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5181 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-06Version 1 pour coqideherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5180 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-06pas ideherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5179 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-06MAJ rpmherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5178 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5177 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5175 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5174 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-05Defaut d'information affichage en cas de notation incompatibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5173 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-05certains id n'etaient pas renommes pour eviter les conflits avec les mots-clesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5172 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5171 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5170 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5169 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-02meilleure presentation des commentaires du traducteurbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5167 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-01[ -d ... ] au lieu de [ -f ... ] sur commit précédéntherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5166 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-01-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5165 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-31*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5164 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 13:08:08 +0000