aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Ints
Commit message (Expand)AuthorAge
* 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-12-02 11:19:28 +0000