aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2007-07-18J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir aspiwack
2007-07-13An update on axiomatization of number classes.emakarov
2007-07-13Added Qpower_plus' and Zpower_Qpowerroconnor
2007-07-13Small cleanupletouzey
2007-07-13Répertoire Numbers poursuit l'objectif entamé en syntaxe V7 dans leherbelin
2007-07-13Deletion of some firstorder calls in FSetAVL: letouzey
2007-07-12Proof for subthery
2007-07-12Deletion of an obsolete file (euclidian division done in old syntax with real...letouzey
2007-07-12normalisation (by closure) was not performed under fixpointsbarras
2007-07-12Proof for succ, add, predthery
2007-07-11Added ForAll_Str_nth_tlroconnor
2007-07-10Big reorganization of romega/ReflOmegaCore.v: towards a modular letouzey
2007-07-06Update of theories/Numbers directory.emakarov
2007-07-05Update on numbers.emakarov
2007-07-05Added Qpower_mult theorem.roconnor
2007-07-03Compatibilité des noms longs de Bool déplacés dans Datatypesherbelin
2007-07-02Correction (partielle) du bug #1587notin
2007-06-29Added the directory theories/Numbers where axiomatizations and implementation...emakarov
2007-06-27- Extensions of FMap(Weak)Facts: letouzey
2007-06-27eqlistA is now equivlistAletouzey
2007-06-26Added zwqipWith.roconnor
2007-06-26additional properties for FMap (and slight rework of SetoidList and FSetPrope...letouzey
2007-06-25Updated Qpow_tac to work on a a more realistic set of exponent values.roconnor
2007-06-22Ajout exist & cie à la table des hints par symétrie avec ex_intro &herbelin
2007-06-21Correction de 2 bugs mineurs: 1 ligne de debug oubliée dans coqdoc, notin
2007-06-21Adding: Field instance for Q.roconnor
2007-06-20ajout de head0 et tail0 en natifbgregoir
2007-06-19safe_shift correct recursionthery
2007-06-19safe_shift recursionthery
2007-06-19safe_shift recursionthery
2007-06-19Adding function is_even, safe_shiftl, safe_shiftrthery
2007-06-19genN.ml syncthery
2007-06-18Correct height computationthery
2007-06-14oups: one file forgotten in my previous commitletouzey
2007-06-14Rework of FSetProperties, in order to add more easily a Properties functor letouzey
2007-06-11undeletion of E_ST and Equal_ST: these records aren't mandatory, but quite us...letouzey
2007-06-08some more properties of fold and elements in FSetPropertiesletouzey
2007-06-08Removed an extra \tacindex occurrence for the tactic discriminate.emakarov
2007-06-07Extension of NArith: Nminus, Nmin, etcletouzey
2007-06-07* For uniformity, FSetAVL uses Implicit Arguments (a bit)letouzey
2007-06-06tail0thery
2007-06-05Gestion espaces dans notation _ = _ :> _herbelin
2007-05-30mul_norm for Q fixedthery
2007-05-28comparison functions should be Defined not Qedletouzey
2007-05-27As suggested by Pierre Casteran, fold for FSets/FMaps now takes a letouzey
2007-05-25fix for bug #1347 (no more Scope pollution by FSets)letouzey
2007-05-22Comparaison JMeq/eq_depherbelin
2007-05-21Added Z and Q implementations with int31.aspiwack
2007-05-21add_mul_pos uses int31 onlythery
2007-05-15pos_mod fixedthery