aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-04-15* added a subsection to explain the automatic declaration of schemes:vsiles
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-15- Un peu de doc, préparation du CHANGES pour la release.herbelin
2008-04-15typovsiles
2008-04-15fix some bogus calls to id_of_string by the extractionletouzey
2008-04-14BinPos: New version of ~1 and ~0 notations, xH replaced by 1 and proofs cleanupletouzey
2008-04-14oubli sur 10790herbelin
2008-04-14suite 10790 (identificateurs)herbelin
2008-04-14Diverses corrections herbelin
2008-04-14Update doc and remove another overloading of equiv_*.msozeau
2008-04-14Renamings to avoid clashes with definitions in Relation_Definitions, nowmsozeau
2008-04-14Fix setoid tests, use red for a Setoid_Theory lemma, and Parametricmsozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-12Désactivation du dumping des notations quand funind appelle lesherbelin
2008-04-12Document the new setoid rewrite tactic, and fix a few things whilemsozeau
2008-04-12Add the ability to specify what to do with free variables in instancemsozeau
2008-04-12Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.msozeau
2008-04-11Check that no evars remain in instance types earlier at Instancemsozeau
2008-04-09Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicitmsozeau
2008-04-09Verify Setoid is loaded before doing anything.msozeau
2008-04-09Fixes in new Morphisms files. msozeau
2008-04-09Fix evar bugs in type classes:msozeau
2008-04-09contradict can now handle False hypothesis in the spirit of contradictionletouzey
2008-04-09Correction bug List.map2 dans Case12.vherbelin
2008-04-09Fix the last compilation problemmsozeau
2008-04-09Fix compilation problemmsozeau
2008-04-08correction of bug 1829jforest
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
2008-04-08Ajout d'options a coqdoc pour l'entete htmlnotin
2008-04-07Fix big de Bruijn bug in mutually recursive definitions.msozeau
2008-04-06Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :herbelin
2008-04-05Suite 10760herbelin
2008-04-05- Retour en arrière sur la capacité du nouvel apply à utiliser lesherbelin
2008-04-05Minor fixes: msozeau
2008-04-04Mise en place d'une extension de apply pour que celui-ci sacheherbelin
2008-04-04A file that can be loaded when a migration from Set to Type is desiredletouzey
2008-04-04Correction problème de compil (blast.ml)herbelin
2008-04-04- Relâchement de la contrainte de bonne longueur des intropatternsherbelin
2008-04-04Test make 3.81herbelin
2008-04-04Quelques améliorations des intro patterns:herbelin
2008-04-04Erreur ou acceptation silencieuce plutôt qu'avertissement systématique quandherbelin
2008-04-04- Amélioration de la présentation de RIneq, même si un nettoyage desherbelin
2008-04-04Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiherbelin
2008-04-03Essai d'un peu plus de conversion dans apply : suppression de laherbelin
2008-04-03New file FMapFullAVL containing the balancing proofs about FMapAVL:letouzey
2008-04-03Correction bug 1818, 3eme commentaire. mauvaise generation de substitution a ...soubiran
2008-04-03- Correction d'un bug de coq_makefile sur les variables CAMLLIBS etnotin
2008-04-03Rework of FMapAVL inspired by recent changes of FSetAVL: letouzey
2008-04-03Chgts mineurs:herbelin
2008-04-03Patch sur le typage d'un foncteur applique a un alias.soubiran