aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2008-06-17Fix bug in handling of classes and instances inside sections atmsozeau
2008-06-17Cleanup in subtac_cases, preparing to use improvements on return predicatemsozeau
2008-06-17Fixes w.r.t. let binders in class contexts and Add Parametricmsozeau
2008-06-17Better typeclass error messages, always giving the full set ofmsozeau
2008-06-16Add possibility to match on defined hypotheses, using brackets tomsozeau
2008-06-14Correction bug 1878 (utilisation de extend_evar déplacée là où uneherbelin
2008-06-13CoqIDE: 2 problèmes de undo encore:herbelin
2008-06-13Temporary fix for bug #1876, printing fails because of unresolvedmsozeau
2008-06-13Numéros de version dans la docnotin
2008-06-12Correction d'un problème lié à une interaction entre hyperref etnotin
2008-06-12Changing the definitions of pred and minus in the style of GGwerner
2008-06-12Correction parser révélé par test-suiteherbelin
2008-06-12Compilation Windowsnotin
2008-06-12Remplacement des 'cp' et 'mkdir' par 'install'notin
2008-06-12Confusion sur commit précédent de library. La capture du Not_foundherbelin
2008-06-11Bug dans l'adaptation de library_full_filename lors du débranchementherbelin
2008-06-11Correction bug alias d'alias.soubiran
2008-06-11Prise en compte de l'export des .cmi dans coq_makefilenotin
2008-06-11Optionally (and by default) split typeclasses evars into connected msozeau
2008-06-11now Escape toggles query panejnarboux
2008-06-11MAJ diversesherbelin
2008-06-11Plutôt que de reposer sur le vernacexpr pour détecter les débuts deherbelin
2008-06-11Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".herbelin
2008-06-11escape key now hides panejnarboux
2008-06-11Zpow_facts.Zmult_power: kills a useless hypothesisletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 04:43:00 +0000