aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-07-03Prise en compte de changments dans subtacnotin
2008-07-02Stop using the discrimination net in typeclasses/setoid rewrite, which wasmsozeau
2008-07-02Correct a bug in the coercion code where we did not go under constantsmsozeau
2008-07-02Improved robustness of micromega parser. Proof search of Micromega test-suite...fbesson
2008-07-01Documentation Prop<=Set et Arguments Scope Globalherbelin
2008-07-01Various bug fixes in type classes and subtac:msozeau
2008-07-01correction sur la doc des modulessoubiran
2008-07-01Encore une suite au 11188/11193 (c'était pas un bon jour)herbelin
2008-06-30QMake : alternative equivalences with Qcanon thanks to earlier irreducibility...letouzey
2008-06-30Fichiers oubliés lors du 11188 :-(herbelin
2008-06-29Correction d'un bug dans l'analyse des contraintes non résoluesherbelin
2008-06-29Correction bug "parser" suite changement syntaxeherbelin
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
2008-06-29Préférence donnée aux constantes qui ne sont pas des projectionsherbelin
2008-06-28QMake: Proofs that add_norm and other ..._norm functions produce irreducible ...letouzey
2008-06-27(Partial) fix for bug #1892, adding a missing newline.msozeau
2008-06-27Enhanced discrimination nets implementation, which can now work withmsozeau
2008-06-27Changement de catch_error pour qu'il rattrape les erreurs d'arguments aspiwack
2008-06-27Logo Coq dans coqidenotin
2008-06-26Mauvaise dépendance dans Makefile.docnotin
2008-06-26Oubli lors de la révision #11177notin
2008-06-25Some work on BigQ :letouzey
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-25Report de la révision #11175 de la branche v8.2 vers le trunknotin
2008-06-25Installation de la documentationnotin
2008-06-25Micromega : bugs fixes - renaming of tactics - documentationfbesson
2008-06-25Typo in documentation (isn't it?)glondu
2008-06-25Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...soubiran
2008-06-24Catch a Not_found exception in the Combined Scheme mechanism to hide an uglyvsiles
2008-06-24Suppression de l'option -dump-glob et ajout d'une option -no-globnotin
2008-06-22MAJ fichiers spécifiques trunkherbelin
2008-06-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
2008-06-21Code cleanup in typeclasses, remove dead and duplicated code.msozeau
2008-06-21Correction petit bug sur révision 11159 (res_pf fait un effet de bordherbelin
2008-06-21Fix bug #1889, correct globalization in class declarations.msozeau
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-21Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)herbelin
2008-06-21Various improvements in handling of evars in general and typingmsozeau
2008-06-20typo in a commentletouzey
2008-06-19Little fixes: print unbound variable in error message (patch by Samuelmsozeau
2008-06-19incomplete bugfix for infocorbinea
2008-06-19removed unwanted linebreaks in pretty printingcorbinea
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
2008-06-18Fix bug in implementation of splitting of class constraints.msozeau
2008-06-18Improvements in subtac:msozeau
2008-06-18Compatibility fixes (Add Setoid bug and accidental introduction of amsozeau
2008-06-18meilleur gestion de la fonction de "cache" des alias (declaremods), et correc...soubiran
2008-06-18Detection de l'architecture sous Windows (et sans uname -o)notin
2008-06-18Où l'on se débarrasse de uname -onotin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 09:20:51 +0000