aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-01-16renommage de TAF.v en MVT.vdesmettr
2003-01-16Correction d'un petit bug dans Sup0desmettr
2003-01-16Renommage de RealsB en Rbasedesmettr
2003-01-16Renommage de Rbase.v en RIneq.vdesmettr
2003-01-15Nouvelle interprétation des nombres réelsdesmettr
2003-01-06bit vectorsfilliatr
2002-12-28Re-installation nombres dans les motifs sur Zherbelin
2002-12-15Une entrée spéciale "annot" pour les piquantsherbelin
2002-12-15Ajout syntaxe '>'herbelin
2002-12-15Ajout syntaxe '>'herbelin
2002-12-15Pas d'associativite pour =_Dherbelin
2002-12-10Compatibilite times1 (suite)herbelin
2002-12-09Nouvelle preuve de times_convert pour nouvelle définition de timesherbelin
2002-12-07Compatibilité times1herbelin
2002-12-06Un axiome en attendant la mise a jour de la preuve de times_convertherbelin
2002-12-06Amélioration sensible de l'efficacité de la multiplicationherbelin
2002-12-03Essai d'introduction d'un scope des typesherbelin
2002-12-02Z_scope doit annuler l'affichage de = entreherbelin
2002-11-29Re-échappement des \ et " dans les token stringherbelin
2002-11-28Simplificationherbelin
2002-11-28Essai de suppression du caractere d'echappement des stringherbelin
2002-11-28Plus de précisionsherbelin
2002-11-27cond_pos -> cond_positivity pour cause de conflit avec posreal...desmettr
2002-11-27Réorganisation de la librairie des réelsdesmettr
2002-11-27Retour sur associativité à droite de * pour compatibilité de prodherbelin
2002-11-26Ne pas cacher les Metas d'une notations, ils peuvent être liant dansherbelin
2002-11-26MAJdesmettr
2002-11-26Theorie 'light' des réelsdesmettr
2002-11-26Explicitation de NONA car sinon LEFTA par défaut; déplacement dans 5herbelin
2002-11-26Plus d'indication pour le gestionnaire de niveauxherbelin
2002-11-26Correction affichage entiers en cas d'échecherbelin
2002-11-26Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiquesherbelin
2002-11-26Bug niveauherbelin
2002-11-25Rétablissement affichage des entiers de natherbelin
2002-11-25Retablissement SynDef Value/Errorherbelin
2002-11-25Oubliherbelin
2002-11-24Traitement des parenthèses de nat au niveau du printerherbelin
2002-11-24Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...herbelin
2002-11-24Généralisation de l'utilisation de Notationherbelin
2002-11-24Remplacement de Syntactic Definition par Notationherbelin
2002-11-20Les parenthèses de la notation '(n)' maintemant mises par ML pour un meilleu...herbelin
2002-11-18Definition et proprietes de l'integrale de Riemanndesmettr
2002-11-18Proprietes des fonctions en escalierdesmettr
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-14Oubliherbelin
2002-11-14JMeq now treated as an equality by tactics.courant
2002-11-14nettoyage preuve limit_compcourant
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-23Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pourherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-23 14:35:10 +0000