aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-04-18Correction bug 1835 + correction bug occur-check résultant en unherbelin
2008-04-18pbm avec echofilliatr
2008-04-17Bug squashing day !msozeau
2008-04-17No compatibility notations for andb and co (this restore a correct Print output)letouzey
2008-04-17Prevent the apparition of &&& when printing a (if ... then ... else false)letouzey
2008-04-17tactique gappafilliatr
2008-04-17documentation tactique gappafilliatr
2008-04-17Add almost empty Classes.tex for documentation of type classes.msozeau
2008-04-17Little fixes in setoid_rewrite.msozeau
2008-04-16Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)letouzey
2008-04-16first-order --> firstorder (kills a warning about not being a valid id)letouzey
2008-04-16flottantsfilliatr
2008-04-16Added a function that escapes XML characters in ppcmds.cek
2008-04-15More renamings to avoid clashes (e.g. with CoRN).msozeau
2008-04-15Mises à jour bugs, CHANGES, code mortherbelin
2008-04-15Document CHANGES in setoid rewrite, move DefaultRelation tomsozeau
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