| Age | Commit message (Expand) | Author |
|---|
| 2008-04-05 | - Retour en arrière sur la capacité du nouvel apply à utiliser les | herbelin |
| 2008-04-05 | Minor fixes: | msozeau |
| 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 | - Amélioration de la présentation de RIneq, même si un nettoyage des | herbelin |
| 2008-04-03 | New file FMapFullAVL containing the balancing proofs about FMapAVL: | letouzey |
| 2008-04-03 | Rework of FMapAVL inspired by recent changes of FSetAVL: | letouzey |
| 2008-04-02 | Minor fixes. Use expanded type in class_tactics for Morphism search, to | msozeau |
| 2008-04-01 | Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient | herbelin |
| 2008-04-01 | Correction du bug #1819 | notin |
| 2008-03-31 | - Fix for rewriting under dependent products. | msozeau |
| 2008-03-30 | Modifications diverses et variées : | herbelin |
| 2008-03-29 | Fix test-suite files, change conflicting notation "->rel" and the others | msozeau |
| 2008-03-28 | Improve error handling and messages for typeclasses. | msozeau |
| 2008-03-28 | - Second pass on implementation of let pattern. Parse "let ' par [as x]? | msozeau |
| 2008-03-28 | Correction du bug 1816 (ajout d'un lemme dans Znat) et suppression | notin |
| 2008-03-27 | - notations &&& and ||| equivalent to andb and orb, | letouzey |
| 2008-03-27 | Various fixes on typeclasses: | msozeau |
| 2008-03-25 | Interpret patterns for hypotheses types in match goal in type_scope (if not a | msozeau |
| 2008-03-23 | Fix a bug found by B. Grégoire when declaring morphisms in module | msozeau |
| 2008-03-23 | Nettoyage Wf.v et unification (suite remarques faites sur cocorico) | herbelin |
| 2008-03-23 | Commit d'une preuve de l'axiome d'Archimède qui traînait dans mes placards. | herbelin |
| 2008-03-23 | Une passe sur les réels: | herbelin |
| 2008-03-22 | Compatibility fixes, backtrack on definitions of reflexive, | msozeau |
| 2008-03-21 | One more AVL reorganisation: separate pure functions from proofs + functional... | letouzey |
| 2008-03-21 | Some "if then else" instead of orb and andb, in order to vm_compute lazily | letouzey |
| 2008-03-20 | Add a flag to control rewriting under lambdas. Otherwise makes some | msozeau |
| 2008-03-20 | still some useless invariants in FSetAVL | letouzey |
| 2008-03-19 | migration of the old IntMap library from StdLib to a user contrib (Cachan/Int... | letouzey |
| 2008-03-19 | Coq.Relations.Relations can move back to its short name | letouzey |
| 2008-03-19 | Do another pass on the typeclasses code. Correct globalization of class | msozeau |
| 2008-03-18 | Implementation of rewriting under lambdas. Tested on exists only. | msozeau |
| 2008-03-18 | Correct implementation of normalization of signatures using setoid | msozeau |
| 2008-03-17 | Add the possibility of specifying constants to unfold for typeclass | msozeau |
| 2008-03-16 | Removed unneeded tactics from RelationClasses. Use | msozeau |
| 2008-03-16 | Using the "relation" constant made some unifications fail in the new | msozeau |
| 2008-03-16 | Misc: Add test for bug 1704, now closed. Add usual syntax for lists in | msozeau |
| 2008-03-16 | Reorganize Program and Classes theories. Requiring Setoid no longer sets | msozeau |
| 2008-03-16 | Minor fixes on setoid rewriting. Now uses definitions of [relation] and | msozeau |
| 2008-03-15 | Reorganisation of FSetAVL (consequences of remarks by B. Gregoire) | letouzey |
| 2008-03-15 | Do a second pass on the treatment of user-given implicit arguments. Now | msozeau |
| 2008-03-14 | Suppress some warnings by writing ugly Coq.Relations.Relations in some .v | letouzey |
| 2008-03-09 | Add a missing morphism declaration that turns morphisms on R ==> R' to | msozeau |
| 2008-03-08 | Fix bugs that were reopened due to the change of setoid | msozeau |
| 2008-03-07 | f_equal, revert, specialize in ML, contradict in better Ltac (+doc) | letouzey |
| 2008-03-07 | repair FSets/FMap after the change in setoid rewrite | letouzey |
| 2008-03-07 | Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part | msozeau |
| 2008-03-06 | Plug the new setoid implemtation in, leaving the original one commented | msozeau |
| 2008-03-06 | Coquille vraisemblablement introduite par la révision 10628 | notin |
| 2008-03-06 | Syntax changes in typeclasses, remove "?" for usual implicit arguments | msozeau |
