aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
...
* 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
* Derivation of (exists x : A, P x) -> {x : A | P x} for decidable PGravatar emakarov2007-01-23
* Clarification redondance Axiome du choix unique/descriptionGravatar herbelin2007-01-22
* Add f_equal case for 6 arguments.Gravatar msozeau2007-01-02
* Remplacement axiome JMeq_eq dans BinPos par eq_dec_eq sur type àGravatar herbelin2006-12-28
* Remplacement de la définition de Pind et Prec par une définitionGravatar herbelin2006-12-28
* Changement dans ring et field, beaucoup de correction d'erreurs,Gravatar bgregoir2006-12-15
* Dépendence inutileGravatar herbelin2006-12-12
* AllÃègement de syntxe suite à l'introduction de l'unif patternGravatar herbelin2006-12-12
* Bug nommage Zgt_trans_succGravatar herbelin2006-12-12
* correction Open Local Scope (Ring)Gravatar bgregoir2006-12-11
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* fixes PR#1269 about function: there is no reason well founded induction isGravatar bertot2006-11-05
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* LegacyRfield was opening R_scopeGravatar barras2006-10-30
* simplif de la partie ML de ring/fieldGravatar barras2006-10-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 01:27:42 +0000