aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-05-26Résolution bug #1850 sur notations avec niveaux inconnus deherbelin
2008-05-26Fix bashism in doc generation.glondu
2008-05-26Bug undo CoqIDE sur Endherbelin
2008-05-26the -g option is not recongnized in ocaml < 3.10.0jforest
2008-05-25- Nouvelle option "Set Printing Existential Instances" pour forcerherbelin
2008-05-24- Prise en compte des frozen state de Coq autant que possible pourherbelin
2008-05-24Ajout de la possibilité d'utiliser fix/cofix dans les notations.herbelin
2008-05-23doc of coqchk + improved module cache and computation of module setsbarras
2008-05-23Cyclic31 : replace the ugly time-consuming brute-force proof by a reasonable ...letouzey
2008-05-23- Fix bug #1858, Hint Unfold calling the wrong locate function.msozeau
2008-05-23Nouvelle doc pour les modules.soubiran
2008-05-23(Not completely finished) proofs that int31 integers fulfill the CyclicAxioms...letouzey
2008-05-22Strategy commands are now exportedbarras
2008-05-22fixed dependency problems with the checkerbarras
2008-05-22writing a match on a digit via syntax "if ... then ... else" is not a good id...letouzey
2008-05-22Proposition for a almost-bitsize-independent Int31.v (joint work with J. Voui...letouzey
2008-05-22QRewrite is now obsolete. It was containing manual ltac stuffletouzey
2008-05-22Should fix the dependancy issue mentioned by J.Forest about NMake: letouzey
2008-05-22switch theories/Numbers from Set to Type (both the abstract and the bignum pa...letouzey
2008-05-22improved coqchk targetsbarras
2008-05-22added coqchk to the main Makefile and a make variable VALIDATE to check the v...barras
2008-05-21refined the conversion oraclebarras
2008-05-21refined the conversion oraclebarras
2008-05-21Désactivation affichage image coqide en attendant un barcelosherbelin
2008-05-21Correction bugs ide undo et highlight (suite à typos)herbelin
2008-05-20Correction d'un bug de l'unification pattern qui oubliait d'expanserherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 19:12:11 +0000