aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
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
2007-05-15Correction de sqrt312 (racine carree d'un nombre represente comme un aspiwack
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-04-28Déplacement des opérations sur bool dans l'état initialherbelin
2007-04-25Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création herbelin
2007-04-17Correction du bug #1510notin
2007-04-13Correction bug #1499notin
2007-04-12Transparency of Z_lt_le_decnotin
2007-04-06simplier version of tail_plusletouzey
2007-04-02Added back the tactics [apply -> ident], etc. to Tactics.v afteremakarov
2007-04-02Réparation de NArith/BinPos.v suite au commit #9739notin
2007-04-01Removed the definition of extensions of apply to equivalencesemakarov
2007-03-30Added the following theorems to BinPos:emakarov
2007-03-30Added new tactics for applying equivalences (iff) to Tactics.v:emakarov
2007-03-26stupid me: ?f two times in a patternletouzey
2007-03-26PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ...letouzey
2007-03-15Typosherbelin
2007-03-14Removed an unnecessary argument (p : positive) in Prect_base.emakarov
2007-03-12Proof simplification for eq_nat_dec et le_lt_dec: induction over letouzey
2007-03-08Transparence de eq_dec et lt_dec daans OrderedTypeFactsnotin
2007-02-28FSetInterface: new item choose_equal in the spec S (request of P. Casteran)letouzey
2007-02-19Ajouts de lemmes dans Min et Maxnotin
2007-02-12Autres passages de Set à Type dans Relations et Wellfoundedherbelin
2007-02-07Backtrack sur le passage de Set à Type pour l'ordre lexicographiqueherbelin
2007-02-06Passage de Set à Type dans Relations et Wellfoundedherbelin
2007-01-31Correction typo eq_rec_eq (cf bug #1339)herbelin