aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2003-10-13Argument implicite pour None, error, exceptherbelin
2003-10-13Notations pour l'exponentiationherbelin
2003-10-13Enregistrement '^' en v8herbelin
2003-10-11mise a jour nouvelle syntaxebarras
2003-10-10nat_scope ouvert par defautherbelin
2003-10-10identity est equivalent sur Type (sauf sans argument)herbelin
2003-10-10type_scopeherbelin
2003-10-10Suppression de definitions equivalentesherbelin
2003-10-10Notation '^'herbelin
2003-10-10Plus d'Eval Computeherbelin
2003-10-10MAJ commentairesherbelin
2003-10-10Delimiters N devient 'nat'herbelin
2003-10-10changement nouvelle syntaxe (pt fixes)barras
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2003-10-10Renommage en v8 de PolyList en List et List en MonoListherbelin
2003-10-03Cacher les .v8herbelin
2003-10-01Retour sur la version non optimisee de 'add' pour compatibilite; renommage Un...herbelin
2003-09-30'_ = _ = _' maintenant predefini, meme en V7herbelin
2003-09-28une induction de moins dans lt_eq_lt_decletouzey
2003-09-28well_founded_induction de nouveau transparentletouzey
2003-09-26'Open Local Scope' en attendant que le core_scope sache se mettre devant impl...herbelin
2003-09-26Induction -> NewInduction; '++' pour appherbelin
2003-09-26Passage de Destruct a NewDestruct; '-' pour negbherbelin
2003-09-26Structuration de fast_integer en operations sur positive, proprietes des oper...herbelin
2003-09-25add_x_x de fast_integer vers auxiliaryherbelin
2003-09-25Retour provisoire a une sectionherbelin
2003-09-24Suppression section, ce qui evite de repliquer les declarations d'Infixherbelin
2003-09-24Destruct/Induction -> NewDestruct/NewInductionherbelin
2003-09-24Destruct -> NewDestructherbelin
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
2003-09-23Remplacement de Induction/Destruct par NewInduction/NewDestructherbelin
2003-09-23Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...herbelin
2003-09-22traducteur: affiche les commentaires a l'interieur des commandesbarras
2003-09-22Implicits maintenant au courant pour l'affichageherbelin
2003-09-22Deplacement de lemmes de IntMap vers ZArithherbelin
2003-09-21Changement de la politique de V8only: V8only tout seul signifieherbelin
2003-09-21Conflit de nom Pplus dans positive et dans polynomial (de ring)herbelin
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-21Les notations 'x <= y <= z' sont réservées et s'appliquent maintenant aussi...herbelin
2003-09-21Nettoyageherbelin
2003-09-19'::' est deja pris en V7herbelin
2003-09-19Section et report Infix hors sectionherbelin
2003-09-19Plus besoin de V7only [ Import ... ] pour l'affichage des notations par le tr...herbelin
2003-09-19Ajout notation :: pour consherbelin
2003-09-19Mise en place des V8Notation et V8Infix pour declarer des notations en v8 mem...herbelin
2003-09-12Suppression DatatypesSyntax et PeanoSyntax qui était videsherbelin
2003-09-12Ajout et MAJ commandes de scopesherbelin
2003-09-12Bind et Delimit pour Rherbelin
2003-09-12Bind et Delimit pour natherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-22 23:10:30 +0000