aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
* Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o...Gravatar emakarov2007-10-04
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
* BigZ now are provedGravatar thery2007-10-03
* The following now compiles: abstract integers with plus, minus and times, bin...Gravatar emakarov2007-10-02
* Now NMake is provedGravatar thery2007-10-02
* Added the compilation of theories/Numbers to Makefile.common. The following t...Gravatar emakarov2007-10-01
* Nouvelle mise à jourGravatar herbelin2007-10-01
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* Creation of a new token PATTERNIDENT (?ident) for intro patterns, soGravatar glondu2007-09-28
* Oubli dans Setoid.vGravatar notin2007-09-28
* Découpage de Setoid.vGravatar notin2007-09-27
* Reals: prod_f_SO inclut f(0) dans le produit et devient prod_f_R0Gravatar herbelin2007-09-27
* added a lemma to prove inj_pair2 when eq_dec is available.Gravatar vsiles2007-09-26
* An update on theories/Numbers.Gravatar emakarov2007-09-25
* Update on theories/NumbersGravatar emakarov2007-09-21
* Update on theories/Numbers. Natural numbers are mostly complete,Gravatar emakarov2007-09-21
* - Fixing bug 1703 ("intros until n" falls back on the variable name whenGravatar herbelin2007-09-21
* Changed the definition of Nminus in BinNat.v by removing comparison.Gravatar emakarov2007-09-20
* Update before joining all signatures into one.Gravatar emakarov2007-09-13
* - renaming Qle_shift_recip_r into Qle_shift_inv_r, etcGravatar roconnor2007-09-07
* Adding a few lemmas for reasoning about inequalities over the Gravatar roconnor2007-08-28
* Add more equality tactics. Upgrade program_simpl for discrimination of conjun...Gravatar msozeau2007-08-26
* An update on axiomatic number classes.Gravatar emakarov2007-08-13
* Fix dependency bugs due to Program modules renamings.Gravatar msozeau2007-08-08
* Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vGravatar emakarov2007-08-08
* A better Program documentation. Include it in the generated stdlib doc.Gravatar msozeau2007-08-08
* Move Program tactics into a proper theories/ directory as they are general pu...Gravatar msozeau2007-08-07
* mul and sqrtGravatar thery2007-07-30
* Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n etGravatar notin2007-07-25
* proof of compare addedGravatar thery2007-07-24
* An update on axiomatization of numbers.Gravatar emakarov2007-07-24
* A generic preprocessing tactic zify for (r)omegaGravatar letouzey2007-07-18
* J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir Gravatar aspiwack2007-07-18
* An update on axiomatization of number classes.Gravatar emakarov2007-07-13
* Added Qpower_plus' and Zpower_QpowerGravatar roconnor2007-07-13
* Small cleanupGravatar letouzey2007-07-13
* Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans leGravatar herbelin2007-07-13
* Deletion of some firstorder calls in FSetAVL: Gravatar letouzey2007-07-13
* Proof for subGravatar thery2007-07-12
* Deletion of an obsolete file (euclidian division done in old syntax with real...Gravatar letouzey2007-07-12
* normalisation (by closure) was not performed under fixpointsGravatar barras2007-07-12
* Proof for succ, add, predGravatar thery2007-07-12
* Added ForAll_Str_nth_tlGravatar roconnor2007-07-11
* Big reorganization of romega/ReflOmegaCore.v: towards a modular Gravatar letouzey2007-07-10
* Update of theories/Numbers directory.Gravatar emakarov2007-07-06
* Update on numbers.Gravatar emakarov2007-07-05
* Added Qpower_mult theorem.Gravatar roconnor2007-07-05
* Compatibilité des noms longs de Bool déplacés dans DatatypesGravatar herbelin2007-07-03
* Correction (partielle) du bug #1587Gravatar notin2007-07-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 10:40:05 +0000