aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notations ↵herbelin
(suite) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4053 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4052 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Mise en conformite de la precedence du '-' unaire avec celle de Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4051 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Concentration des notations officielles dans Init/Notations; restructuration ↵herbelin
de Init git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4050 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Nouveaux testsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4049 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4048 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Notationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4047 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Bugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4046 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; réparation local défs récursive dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4045 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4044 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵herbelin
les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21Possibilité de syntaxe conjointement à la définition des inductifs et des ↵herbelin
points-fixes; prise en compte par le traducteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4042 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4041 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20CoqIde: externalsmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4040 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20Prise en compte notation dans Inductif pour traducteurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4039 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20command_windows fixmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4038 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20Extension renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4037 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4036 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Affichage METAherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4035 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Restructutation Hipattern Patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4034 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Restructuration des procédures de filtrageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4032 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19*** empty log message ***monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4031 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19CoqIde : but reset_modfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4030 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19configure et make install s'occupent de CoqIde tout seulsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4029 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19but Require dans une Sectionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4028 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4027 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-16Major Ground tactic update, sensible performance improvementcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4026 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-15table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ↵filliatr
notamment) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4025 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-15class CoqIde donnée à l'application, pour une meilleure intégrationfilliatr
avec le Window Manager git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4024 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4023 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14coqide: .* on start/add \n on eofmonate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4022 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14coqide: load/save file encoding support/monate
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4021 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Amelioration presentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4020 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Amelioration affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4019 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Hack pour ameliorer l'affichage des applications dans les `...` etherbelin
``...`` en les mettant sous forme n-aire, et sans casser la compatibilite des implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4018 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4017 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Suppression de 'R' dans la notation == entreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4016 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Suppression de 'R' dans la notation == entreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4015 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-14Deplacement lemmes sur fact de Reals vers Arithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4014 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Nouveaux lemmesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4013 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Nouveaux lemmes (sur proposition de Nijmegen)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4012 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Affichage commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4011 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Nouveaux lemmes (sur proposition de Nijmegen)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4010 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Rien d'importantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4009 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Notations arithmetiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4008 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Orthographe anglaise - typosherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4007 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Orthographe anglaiseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4006 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-13Separation entre les propositions de syntaxe - suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4005 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 04:59:56 +0000