aboutsummaryrefslogtreecommitdiff
path: root/theories/Init
AgeCommit message (Expand)Author
2002-11-07Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co...herbelin
2002-10-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
2002-10-22Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...herbelin
2002-10-21Niveau d'affichage sumor/sumbool incohérent avec le parsingherbelin
2002-10-21Prise en compte des délimiteurs dans les motifs de Casesherbelin
2002-10-18Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribsherbelin
2002-10-17Bugs dans la factorisation des règles de parsing de "{ ... } * ..."herbelin
2002-10-17Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribsherbelin
2002-10-14La règle pour parser "(1)", "(2)", ... entre en conflit avec les expressionsherbelin
2002-10-13Mise en place d'ensembles de notations symboliques pour nat, Z et Rherbelin
2002-10-13Nettoyageherbelin
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
2002-10-13Déplacement de + et * aux niveaux de précédence 7 et 6herbelin
2002-07-15Bug de précédenceherbelin
2002-07-11Hack pour parser '{x:T|P}*B' sans parenthesesherbelin
2002-05-29Utilisation d'Infix/Distfix autant que possibleherbelin
2002-05-14petite erreur de syntaxebarras
2002-05-14ajout des theoremes eqT_rec_r et eqT_rect_r pour Rewritebarras
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
2002-05-07lemmes plus_O_n et plus_Sn_m (pour Yves)filliatr
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-02-22Docherbelin
2002-02-19Uniformisation des theoremes dans Set et Type (def. de Acc_rect etbarras
2002-02-14option -dump-glob pour coqdocfilliatr
2002-02-14Syntaxe IF then else au lieu de either and_then or_elsebarras
2002-01-31changement generation de schema d'elimination, False_rec est primitif, Constr...mohring
2002-01-29modification de la definition des def inductives unitaires et autorisation d'...mohring
2002-01-10Modifs incongrues dans le précédent commitherbelin
2002-01-09MAJ des Id pour coqwebherbelin
2001-11-14Suppression d'Export redondantsherbelin
2001-10-24Suppression de Logic_Type.sigT, redondant avec Specif.sigTherbelin
2001-09-27and_rec redondantletouzey
2001-09-20Transparentbarras
2001-09-19Deplacement des setoides.clrenard
2001-09-18Modification de l'emplacement des fichiers pour les setoides.clrenard
2001-08-30Fin de la modif Exc/optionmohring
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-05-29Correction d'un bug du pretty-printclrenard
2001-05-15Modification pour passage p-automatesmohring
2001-04-11documentation automatique de la bibliothèque standardfilliatr
2001-03-30Introduction d'une preuve de False_recmohring
2001-03-15entetesfilliatr
2000-12-21Bug d'affichage à cause des << ... >>herbelin
2000-11-21separation calcul des implicites et declaration des constantes / inductifs / ...filliatr
2000-11-20Bug dans la règle de syntaxe de ex2herbelin
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
2000-10-18Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...herbelin
2000-07-28Plus de piquants dans les actions des grammaires; nom de la grammaire pris co...herbelin