aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-06-30Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Recordherbelin
2007-06-30- Ajout de la possibilité d'utiliser la notation Record pour lesherbelin
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-26killing some more non-exhaustive patternsletouzey
2007-06-26kill an ugly warning about a non-exhaustive patternletouzey
2007-06-26Oups: thanks to ./configure -reals no, I was not building the whole dependenc...letouzey
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-21Simplification de la construction du .depend:notin
2007-06-21Correction de plusieurs bugs de l'export XML (utilisation d'un type deherbelin
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-19typo faqherbelin
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-14Correction du bug sur make dependnotin
2007-06-14Add Solve All Obligations command, fix bug in inequality generation introduce...msozeau
2007-06-11undeletion of E_ST and Equal_ST: these records aren't mandatory, but quite us...letouzey
2007-06-09Various Program fixes, multiple pattern matches, aliases. Fix bug in coercion...msozeau
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-07Ajout doc clear sans argumentherbelin
2007-06-07Unification des types + clause filtrage manquante + uniformisation localeherbelin
2007-06-06Toujours l'unification de apply : nouveau raffinement pour ne testerherbelin
2007-06-06tail0thery
2007-06-05Gestion espaces dans notation _ = _ :> _herbelin
2007-06-05Amélioration de la complexité de auto (l'utilisation des types dansherbelin
2007-05-30Corrections dans le Print Assumption. Les definitions locales ("Let") aspiwack
2007-05-30Memory optimisation for modules and constrs substitutions.soubiran
2007-05-30mul_norm for Q fixedthery
2007-05-29Corrected the treatment of negative numbers for the bigZ parser. And aspiwack
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-05-28comparison functions should be Defined not Qedletouzey
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
2007-05-28Retour à un message d'erreur d'apply qui montre un échec sans sans réduction herbelin
2007-05-28Réaffichage des Structure/Record sous la forme Recordherbelin
2007-05-27As suggested by Pierre Casteran, fold for FSets/FMaps now takes a letouzey