aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* 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
* Added the directory theories/Numbers where axiomatizations and implementation...Gravatar emakarov2007-06-29
* - Extensions of FMap(Weak)Facts: Gravatar letouzey2007-06-27
* eqlistA is now equivlistAGravatar letouzey2007-06-27
* Added zwqipWith.Gravatar roconnor2007-06-26
* additional properties for FMap (and slight rework of SetoidList and FSetPrope...Gravatar letouzey2007-06-26
* Updated Qpow_tac to work on a a more realistic set of exponent values.Gravatar roconnor2007-06-25
* Ajout exist & cie à la table des hints par symétrie avec ex_intro &Gravatar herbelin2007-06-22
* Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, Gravatar notin2007-06-21
* Adding: Field instance for Q.Gravatar roconnor2007-06-21
* ajout de head0 et tail0 en natifGravatar bgregoir2007-06-20
* safe_shift correct recursionGravatar thery2007-06-19
* safe_shift recursionGravatar thery2007-06-19
* safe_shift recursionGravatar thery2007-06-19
* Adding function is_even, safe_shiftl, safe_shiftrGravatar thery2007-06-19
* genN.ml syncGravatar thery2007-06-19
* Correct height computationGravatar thery2007-06-18
* oups: one file forgotten in my previous commitGravatar letouzey2007-06-14
* Rework of FSetProperties, in order to add more easily a Properties functor Gravatar letouzey2007-06-14
* undeletion of E_ST and Equal_ST: these records aren't mandatory, but quite us...Gravatar letouzey2007-06-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 21:03:37 +0000