aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* fixed universes bug related to module inclusionGravatar barras2008-04-22
* test module include w.r.t. universe constraintsGravatar barras2008-04-21
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21
* - Correct unification for the rewrite variant of setoid_rewrite,Gravatar msozeau2008-04-21
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Addded the "Dump Tree" command.Gravatar cek2008-04-21
* corection bug #1837Gravatar soubiran2008-04-21
* Correction bug 1838 + doc modules.Gravatar soubiran2008-04-21
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
* Add the ability to give a transparent_state for conversion, toGravatar msozeau2008-04-20
* Test pour compilation native camlp5Gravatar herbelin2008-04-19
* Pour engendrer version.tex, adoption de printf qui, au contraire deGravatar herbelin2008-04-18
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 22:54:40 +0000