aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2007-08-26Fix evars bug in mutual fixpoints with implicit types and bug in inequalities...msozeau
2007-08-26Add more equality tactics. Upgrade program_simpl for discrimination of conjun...msozeau
2007-08-25Extension et documentation de real_clean/evar_define dans evarutil.ml:herbelin
2007-08-24Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...herbelin
2007-08-24Utilisation plus précise de la contrainte de type pour interpréter lesherbelin
2007-08-22Correction du bug #1634 + ajout de bugs dans la test-suitenotin
2007-08-22Save IS NOT the same Defined ....msozeau
2007-08-22- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)herbelin
2007-08-22Ajout d'un warning losrqu'un nom de bibliothèque est ambigünotin
2007-08-20Modification de l'initialisation des chemins de la librairie standardnotin
2007-08-20Typo in INSTALL instructionslmamane
2007-08-20Erreur de copier/coller dans la section Guardednotin
2007-08-16Correction du bug #1322notin
2007-08-16Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;notin
2007-08-13An update on axiomatic number classes.emakarov
2007-08-13Correction (partielle) bug #1052 (coqdoc supprime les fins de ligne après un...notin
2007-08-13Correction du bug #1635notin
2007-08-10Ajout d'un exemple d'inversion des dépendances dans le prédicat commeherbelin
2007-08-10- Correction d'un bug de de Bruijn dans abstract_predicate (lié auherbelin
2007-08-10Typonotin
2007-08-10Modification de la test suite pour intégrer des tests spécifiques auxnotin
2007-08-09Modification de control_only_guard, qui utilise maintenantnotin
2007-08-08Fix dependency bugs due to Program modules renamings.msozeau
2007-08-08Several simple new theorems in ZArith/BinInt.v and ZArith/Zbool.vemakarov
2007-08-08Add a test case for the new "dependent" induction tactics.msozeau
2007-08-08A better Program documentation. Include it in the generated stdlib doc.msozeau
2007-08-07Move Program tactics into a proper theories/ directory as they are general pu...msozeau
2007-08-07Add a new tactic to generalize an instantiated inductive predicate adding equ...msozeau
2007-08-07Build system: _really_ don't recurse into VCS metadata for file listslmamane
2007-08-07Build system:lmamane
2007-08-01Build system: BSD compatibility: do not use -printf action of findlmamane
2007-07-30mul and sqrtthery
2007-07-26Corrected the reference to glob.dump, which is used to create stdlib/index-bo...emakarov
2007-07-25Add glob.dump to Makefile the recommended way and document thelmamane
2007-07-25Modifications de la construction de la documentation de la librairienotin
2007-07-25Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n etnotin
2007-07-24fixed bug 1448 and 1674barras
2007-07-24proof of compare addedthery
2007-07-24fixed bug 1675: computing carrier from the relation type was not rightbarras
2007-07-24Declarative language: fixed the generation of fixpoints for induction proofs.corbinea
2007-07-24An update on axiomatization of numbers.emakarov
2007-07-23removed thesisbarras
2007-07-19Documentation of Program and its tactics, fix enormous interaction bug due to...msozeau
2007-07-19some more svn:ignore propertiesletouzey
2007-07-18A generic preprocessing tactic zify for (r)omegaletouzey
2007-07-18Makefile: slightly cleaner version of r10026lmamane
2007-07-18Makefile: don't mention bin/coqtop.byte twice to make when BEST=byte, it comp...lmamane
2007-07-18Cleanly refuse to operate in the presence of unsaved changes in emacslmamane
2007-07-18Affichage de "thesis" seulement en mode déclaratifherbelin
2007-07-18Oups... Use shell-variable syntax in shell commands.lmamane
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 13:56:24 +0000