aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
2003-12-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5163 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-30option -strict-implicit pas reconnuebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5162 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-30ameliorations coqidecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5160 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5159 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-28MAJ 8.0herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5158 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-27Protection contre l'echec des tests parser pour la distribherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5157 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-27Suppression en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5156 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-12-27MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5155 85f007b7-540e-0410-9357-904b9bb8a0f7