aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-05-20Corrections d'erreurs rapportées par Frédéric Besson sur le précédentherbelin
2008-05-20added checker to svn:ignorebarras
2008-05-20also fixed conversion of the checkerbarras
2008-05-20Cleanup build_new, remove unneeded try-with and debug interaction ofmsozeau
2008-05-20Léger backtrack sur commit coqide précédent (si la commande à annulerherbelin
2008-05-20Fixed coqide bug #1856 that was introduced in revision 10915.herbelin
2008-05-20Retrait d'un test commité par erreur en 10947herbelin
2008-05-19MAJ créditsherbelin
2008-05-19Intégration de micromega ("omicron" pour fourier et sa variante sur Z,herbelin
2008-05-19Fix globalization bug in class_tactics and refactorize instancemsozeau
2008-05-19Fix caml debug flags configuration, -g works with the native compiler onlymsozeau
2008-05-19Minor improvement: group stuff about carry apart from stuff about zn2zletouzey
2008-05-19Thanks to Matthieu's commit 10941, Ad-hoc tactics contained in QRewrite are n...letouzey
2008-05-17ZModulo: Z viewed modulo 2^digits implements CyclicAxiomsletouzey
2008-05-17Fix a de Bruijn bug in setoid_rewrite when rewriting undermsozeau
2008-05-16Filename ZnZ (or Z_nZ in a later attempt) is neither pretty nor accurateletouzey
2008-05-16BigNum: more reorganization, mainly moves GenXYZ to DoubleXYZletouzey
2008-05-16Deletion of empty directory TreeModletouzey
2008-05-16ZTreeMod was meant to prove that BigZ correspond to the Integer Axioms.letouzey
2008-05-16More BigNum cleanup: letouzey
2008-05-15In practice, the new setoid rewrite (and the "at" syntax) allows to avoid letouzey
2008-05-15Coq headers + $ in theories/Numbers filesletouzey
2008-05-15Better implementation of the set of instances of a given class as a Cmapmsozeau
2008-05-15Various fixes:msozeau
2008-05-15really fixed Georges\' bugbarras
2008-05-15Oubli lors de la révision 10899 (Bool_nat.vo)notin
2008-05-14Résolution des problèmes ambigus d'inférence du type de retour desherbelin
2008-05-14corrige le bug de Georgesbarras
2008-05-13- Fix bug related to indices of fixpoints.msozeau
2008-05-13debug et nouvelles commandes Dp_prelude et Dp_predefinedfilliatr
2008-05-12MAJ et bricoles diversesherbelin
2008-05-12Fix "not an applied typeclass" error for legitimate classesmsozeau
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-05-11- Changement du code de Zplus pour accomoder ring qui sinon prend uneherbelin
2008-05-10Correction bug #1842 + correction bug initialisation introduit dansherbelin
2008-05-10- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desherbelin
2008-05-10Amélioration de la colorisation, du backtrack et des messages de CoqIDEherbelin
2008-05-09Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]herbelin
2008-05-09Still Ints-->Numbers transition: fix the previous commit about a typoletouzey
2008-05-08Still Ints-->Numbers transition: fix a typo preventing the compilation of BigQletouzey
2008-05-08Autre oubli de la révision 10904herbelin
2008-05-08remove mention of an obsolete limitation of Add Morphismletouzey
2008-05-08Oups, my new version of NMake_gen.ml was relying on a 3.10 feature:letouzey
2008-05-08Suite 10904 (fichiers oubliés)herbelin
2008-05-08** Efficacité, bugs, robustesse CoqIDE **herbelin
2008-05-08Integration of theories/Ints into theories/Numbers, again : better generation...letouzey
2008-05-08Integration of theories/Ints into theories/Numbers, part 3: auto-generation o...letouzey
2008-05-07Integration of theories/Ints into theories/Numbers, part 3: fixing forgotten ...letouzey