| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | Diverses corrections |  herbelin | 2008-04-14 |
| * | Update doc and remove another overloading of equiv_*. |  msozeau | 2008-04-14 |
| * | Renamings to avoid clashes with definitions in Relation_Definitions, now | msozeau | 2008-04-14 |
| * | Fix setoid tests, use red for a Setoid_Theory lemma, and Parametric | msozeau | 2008-04-14 |
| * | Bugs, nettoyage, et améliorations diverses | herbelin | 2008-04-13 |
| * | Désactivation du dumping des notations quand funind appelle les | herbelin | 2008-04-12 |
| * | Document the new setoid rewrite tactic, and fix a few things while | msozeau | 2008-04-12 |
| * | Add the ability to specify what to do with free variables in instance | msozeau | 2008-04-12 |
| * | Adding 'at' to rewrite, as it is already implemented in setoid_rewrite. | msozeau | 2008-04-12 |
| * | Check that no evars remain in instance types earlier at Instance | msozeau | 2008-04-11 |
| * | Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicit | msozeau | 2008-04-09 |
| * | Verify Setoid is loaded before doing anything. | msozeau | 2008-04-09 |
| * | Fixes in new Morphisms files. | msozeau | 2008-04-09 |
| * | Fix evar bugs in type classes: | msozeau | 2008-04-09 |
| * | contradict can now handle False hypothesis in the spirit of contradiction |  letouzey | 2008-04-09 |
| * | Correction bug List.map2 dans Case12.v | herbelin | 2008-04-09 |
| * | Fix the last compilation problem | msozeau | 2008-04-09 |
| * | Fix compilation problem | msozeau | 2008-04-09 |
| * | correction of bug 1829 |  jforest | 2008-04-08 |
| * | - A little cleanup in Classes/*. Separate standard morphisms on | msozeau | 2008-04-08 |
| * | Ajout d'options a coqdoc pour l'entete html |  notin | 2008-04-08 |
| * | Fix big de Bruijn bug in mutually recursive definitions. | msozeau | 2008-04-07 |
| * | Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt : | herbelin | 2008-04-06 |
| * | Suite 10760 | herbelin | 2008-04-05 |
| * | - Retour en arrière sur la capacité du nouvel apply à utiliser les | herbelin | 2008-04-05 |
| * | Minor fixes: | msozeau | 2008-04-05 |
| * | Mise en place d'une extension de apply pour que celui-ci sache | herbelin | 2008-04-04 |
| * | A file that can be loaded when a migration from Set to Type is desired | letouzey | 2008-04-04 |
| * | Correction problème de compil (blast.ml) | herbelin | 2008-04-04 |
| * | - Relâchement de la contrainte de bonne longueur des intropatterns | herbelin | 2008-04-04 |
| * | Test make 3.81 | herbelin | 2008-04-04 |
| * | Quelques améliorations des intro patterns: | herbelin | 2008-04-04 |
| * | Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quand | herbelin | 2008-04-04 |
| * | - Amélioration de la présentation de RIneq, même si un nettoyage des | herbelin | 2008-04-04 |
| * | Protection de rewrite in contre le dépliage des constantes dans w_unify, ce qui | herbelin | 2008-04-04 |
| * | Essai d'un peu plus de conversion dans apply : suppression de la | herbelin | 2008-04-03 |
| * | New file FMapFullAVL containing the balancing proofs about FMapAVL: | letouzey | 2008-04-03 |
| * | Correction bug 1818, 3eme commentaire. mauvaise generation de substitution a ... |  soubiran | 2008-04-03 |
| * | - Correction d'un bug de coq_makefile sur les variables CAMLLIBS et | notin | 2008-04-03 |
| * | Rework of FMapAVL inspired by recent changes of FSetAVL: | letouzey | 2008-04-03 |
| * | Chgts mineurs: | herbelin | 2008-04-03 |
| * | Patch sur le typage d'un foncteur applique a un alias. | soubiran | 2008-04-03 |
| * | Minor fixes. Use expanded type in class_tactics for Morphism search, to | msozeau | 2008-04-02 |
| * | Add the ability to specify the implicit status of section variables and | msozeau | 2008-04-02 |
| * | Typo affichage "simple apply" | herbelin | 2008-04-01 |
| * | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin | 2008-04-01 |
| * | Ajout "simple apply" et "simple eapply" pour apply sans unfold | herbelin | 2008-04-01 |
| * | Finish enhancemenent of return clause inference from tycons, integrating | msozeau | 2008-04-01 |
| * | Enhance handling of parameters in typeclass constraints: permit to specify an... | msozeau | 2008-04-01 |
| * | Add option to set the opacity of obligations to transparent, to be able | msozeau | 2008-04-01 |
herbelin
msozeau
letouzey
jforest
notin
soubiran