aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Correction bug 1835 + correction bug occur-check résultant en unGravatar herbelin2008-04-18
* pbm avec echoGravatar filliatr2008-04-18
* Bug squashing day !Gravatar msozeau2008-04-17
* No compatibility notations for andb and co (this restore a correct Print output)Gravatar letouzey2008-04-17
* Prevent the apparition of &&& when printing a (if ... then ... else false)Gravatar letouzey2008-04-17
* tactique gappaGravatar filliatr2008-04-17
* documentation tactique gappaGravatar filliatr2008-04-17
* Add almost empty Classes.tex for documentation of type classes.Gravatar msozeau2008-04-17
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
* Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)Gravatar letouzey2008-04-16
* first-order --> firstorder (kills a warning about not being a valid id)Gravatar letouzey2008-04-16
* flottantsGravatar filliatr2008-04-16
* Added a function that escapes XML characters in ppcmds.Gravatar cek2008-04-16
* More renamings to avoid clashes (e.g. with CoRN).Gravatar msozeau2008-04-15
* Mises à jour bugs, CHANGES, code mortGravatar herbelin2008-04-15
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
* * added a subsection to explain the automatic declaration of schemes:Gravatar vsiles2008-04-15
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* typoGravatar vsiles2008-04-15
* fix some bogus calls to id_of_string by the extractionGravatar letouzey2008-04-15
* BinPos: New version of ~1 and ~0 notations, xH replaced by 1 and proofs cleanupGravatar letouzey2008-04-14
* oubli sur 10790Gravatar herbelin2008-04-14
* suite 10790 (identificateurs)Gravatar herbelin2008-04-14
* Diverses corrections Gravatar herbelin2008-04-14
* Update doc and remove another overloading of equiv_*.Gravatar msozeau2008-04-14
* Renamings to avoid clashes with definitions in Relation_Definitions, nowGravatar msozeau2008-04-14
* Fix setoid tests, use red for a Setoid_Theory lemma, and ParametricGravatar msozeau2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Désactivation du dumping des notations quand funind appelle lesGravatar herbelin2008-04-12
* Document the new setoid rewrite tactic, and fix a few things whileGravatar msozeau2008-04-12
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
* Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.Gravatar msozeau2008-04-12
* Check that no evars remain in instance types earlier at InstanceGravatar msozeau2008-04-11
* Verify Setoid is loaded only if we're not in Coq.Classes.*. Add explicitGravatar msozeau2008-04-09
* Verify Setoid is loaded before doing anything.Gravatar msozeau2008-04-09
* Fixes in new Morphisms files. Gravatar msozeau2008-04-09
* Fix evar bugs in type classes:Gravatar msozeau2008-04-09
* contradict can now handle False hypothesis in the spirit of contradictionGravatar letouzey2008-04-09
* Correction bug List.map2 dans Case12.vGravatar herbelin2008-04-09
* Fix the last compilation problemGravatar msozeau2008-04-09
* Fix compilation problemGravatar msozeau2008-04-09
* correction of bug 1829Gravatar jforest2008-04-08
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* Ajout d'options a coqdoc pour l'entete htmlGravatar notin2008-04-08
* Fix big de Bruijn bug in mutually recursive definitions.Gravatar msozeau2008-04-07
* Renoncement à rationaliser les Hints "real" vis à vis de Rle/Rge et Rlt/Rgt :Gravatar herbelin2008-04-06
* Suite 10760Gravatar herbelin2008-04-05
* - Retour en arrière sur la capacité du nouvel apply à utiliser lesGravatar herbelin2008-04-05
* Minor fixes: Gravatar msozeau2008-04-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 23:54:18 +0000