aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Ints
Commit message (Expand)AuthorAge
* Adding Zdiv_le_compat_lGravatar thery2008-01-22
* Bug in sqrt321Gravatar thery2008-01-17
* Pour éviter des erreus lors de make doc dues à du code source non taggé en...Gravatar notin2007-12-21
* Petit oubli de thery.Gravatar glondu2007-12-07
* Adding MemoFunction + Lowering HeightGravatar thery2007-12-06
* extensible versionGravatar thery2007-11-21
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...Gravatar letouzey2007-11-06
* In agreement with Laurent Thery, start migration of auxiliary results Gravatar letouzey2007-11-01
* Adding BigQ and proofsGravatar thery2007-10-25
* Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o...Gravatar emakarov2007-10-04
* BigZ now are provedGravatar thery2007-10-03
* Now NMake is provedGravatar thery2007-10-02
* Creation of a new token PATTERNIDENT (?ident) for intro patterns, soGravatar glondu2007-09-28
* - Fixing bug 1703 ("intros until n" falls back on the variable name whenGravatar herbelin2007-09-21
* 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
* 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
* Proof for subGravatar thery2007-07-12
* normalisation (by closure) was not performed under fixpointsGravatar barras2007-07-12
* Proof for succ, add, predGravatar thery2007-07-12
* 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
* tail0Gravatar thery2007-06-06
* mul_norm for Q fixedGravatar thery2007-05-30
* Added Z and Q implementations with int31.Gravatar aspiwack2007-05-21
* add_mul_pos uses int31 onlyGravatar thery2007-05-21
* pos_mod fixedGravatar thery2007-05-15
* Correction de sqrt312 (racine carree d'un nombre represente comme un Gravatar aspiwack2007-05-15
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 05:19:52 +0000