aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* 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
* some more properties of fold and elements in FSetPropertiesGravatar letouzey2007-06-08
* Removed an extra \tacindex occurrence for the tactic discriminate.Gravatar emakarov2007-06-08
* Extension of NArith: Nminus, Nmin, etcGravatar letouzey2007-06-07
* * For uniformity, FSetAVL uses Implicit Arguments (a bit)Gravatar letouzey2007-06-07
* tail0Gravatar thery2007-06-06
* Gestion espaces dans notation _ = _ :> _Gravatar herbelin2007-06-05
* mul_norm for Q fixedGravatar thery2007-05-30
* comparison functions should be Defined not QedGravatar letouzey2007-05-28
* As suggested by Pierre Casteran, fold for FSets/FMaps now takes a Gravatar letouzey2007-05-27
* fix for bug #1347 (no more Scope pollution by FSets)Gravatar letouzey2007-05-25
* Comparaison JMeq/eq_depGravatar herbelin2007-05-22
* 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
* Déplacement des opérations sur bool dans l'état initialGravatar herbelin2007-04-28
* Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création Gravatar herbelin2007-04-25
* Correction du bug #1510Gravatar notin2007-04-17
* Correction bug #1499Gravatar notin2007-04-13
* Transparency of Z_lt_le_decGravatar notin2007-04-12
* simplier version of tail_plusGravatar letouzey2007-04-06
* Added back the tactics [apply -> ident], etc. to Tactics.v afterGravatar emakarov2007-04-02
* Réparation de NArith/BinPos.v suite au commit #9739Gravatar notin2007-04-02
* Removed the definition of extensions of apply to equivalencesGravatar emakarov2007-04-01
* Added the following theorems to BinPos:Gravatar emakarov2007-03-30
* Added new tactics for applying equivalences (iff) to Tactics.v:Gravatar emakarov2007-03-30
* stupid me: ?f two times in a patternGravatar letouzey2007-03-26
* PositiveOrderedTypeBits is now formulated to be a UsualOrderedType, not only ...Gravatar letouzey2007-03-26
* TyposGravatar herbelin2007-03-15
* Removed an unnecessary argument (p : positive) in Prect_base.Gravatar emakarov2007-03-14
* Proof simplification for eq_nat_dec et le_lt_dec: induction over Gravatar letouzey2007-03-12
* Transparence de eq_dec et lt_dec daans OrderedTypeFactsGravatar notin2007-03-08
* FSetInterface: new item choose_equal in the spec S (request of P. Casteran)Gravatar letouzey2007-02-28
* Ajouts de lemmes dans Min et MaxGravatar notin2007-02-19
* Autres passages de Set à Type dans Relations et WellfoundedGravatar herbelin2007-02-12
* Backtrack sur le passage de Set à Type pour l'ordre lexicographiqueGravatar herbelin2007-02-07
* Passage de Set à Type dans Relations et WellfoundedGravatar herbelin2007-02-06
* Correction typo eq_rec_eq (cf bug #1339)Gravatar herbelin2007-01-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 22:34:14 +0000