aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2003-05-05Corrige Bug (PR#290)coq
2003-04-30majfilliatr
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
2003-04-29Prise en compte des syntaxes v8 dans Uninterpreted Notationherbelin
2003-04-29coqide: search forw+backmonate
2003-04-29Mise en place d'un 2ème traducteur à l'essai (activable avec -ftranslate2)herbelin
2003-04-29Blancsherbelin
2003-04-29Notationsherbelin
2003-04-29Implicit Typesherbelin
2003-04-29Ajout ChoiceFactsherbelin
2003-04-29Blancsherbelin
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et n:=...herbelin
2003-04-29Factorisation des produits de même type; parenthèses autour des x:=c et n:=...herbelin
2003-04-29Moins de ' ' à l'affichageherbelin
2003-04-29En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...herbelin
2003-04-29Bug fermeture de stdoutherbelin
2003-04-29Ajout is_ident_tailherbelin
2003-04-28coqide: search forwardmonate
2003-04-28Localisation erreurs TacAlias; Globalisation moins tolérante dans lesherbelin
2003-04-28bug concernant les projecteurs de Record avec args logiquesletouzey
2003-04-28ajout d'une elimination simplifiée Acc_iter pour Accletouzey
2003-04-28adaptation a Acc_iterletouzey
2003-04-28Un principe light d'elimination de Acc, suivant les remarques de Yves Bertotletouzey
2003-04-28fichier de pref coq IDE en ASCII (ENFIN)filliatr
2003-04-28majfilliatr
2003-04-27Ce que Try récupèreherbelin
2003-04-27Affichage des Fix contenant des Let dans leur context (ce que la tactique Fix...herbelin
2003-04-27Reparation affichage LetTacherbelin
2003-04-26bugfix in Ground tacticcorbinea
2003-04-26majfilliatr
2003-04-25Added the Ground tactic.corbinea
2003-04-25utf8.vmonate
2003-04-25new utf8.vmonate
2003-04-25extension des caracteres UTF 8 autorises dans les symbolesfilliatr
2003-04-24*** empty log message ***monate
2003-04-24coqide : line number modemonate
2003-04-24*** empty log message ***monate
2003-04-22Coqide : bug undomonate
2003-04-22coqide : progressbarmonate
2003-04-18majfilliatr
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
2003-04-17MAJherbelin
2003-04-17Diversherbelin
2003-04-17<> maintenant standardherbelin
2003-04-17Intégration DatatypesSyntax à Datatypesherbelin
2003-04-17Syntaxe 'x=y:>T'herbelin
2003-04-17Ajout "at next level" dans Notationherbelin
2003-04-17commentairesherbelin
2003-04-17Ooopsletouzey
2003-04-17majfilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 09:18:26 +0000