aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* repair FSets/FMap after the change in setoid rewriteGravatar letouzey2008-03-07
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Coquille vraisemblablement introduite par la révision 10628Gravatar notin2008-03-06
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* even_2n et odd_S2n deviennent transparents (chez moi, ça empêchait de compi...Gravatar notin2008-03-06
* Backtrack sur la révision #10401 : suppression de le_minus de la base de hin...Gravatar notin2008-03-05
* still one more substituion s/Set/Type/Gravatar letouzey2008-03-04
* one more substitution s/Set/Type/Gravatar letouzey2008-03-04
* migration from Set to Type of FSet/FMap + some dependencies...Gravatar letouzey2008-03-04
* A fix for compilation of FMapFacts (a story of impl arg for Logic.eq)Gravatar letouzey2008-03-02
* Marche-arrière sur la suppression de l'hypothèse inutile de Rpower_OGravatar herbelin2008-03-01
* Argumentation plus poussée de pourquoi on retire la condition x>0 dansGravatar herbelin2008-02-29
* Some suggestions about FMap by P. Casteran: Gravatar letouzey2008-02-28
* cardinal is promoted to the rank of primitive member of the FMap interfaceGravatar letouzey2008-02-28
* Do not open type_scope in SetoidClass.Gravatar msozeau2008-02-28
* Fix compilation problem (hopefully).Gravatar msozeau2008-02-28
* Nicer third spec of choose. Gravatar letouzey2008-02-28
* For more uniformity, use implicits in FSetAVLGravatar letouzey2008-02-27
* Application patch #1807 sur hypothèse inutile de Rpower_OGravatar herbelin2008-02-27
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* Backtrack changes on eauto, move specialized version of eauto inGravatar msozeau2008-02-14
* Debugging of the class_setoid tactic and eauto. Prepare for move fromGravatar msozeau2008-02-13
* Essai de prise en compte de delta dans unify_0 (même sur termes non clos). Gravatar herbelin2008-02-13
* Backport Program Instance into Instance. Proper early error message ifGravatar msozeau2008-02-10
* Proposal of a nice notation for constructors xI and xO of type positiveGravatar letouzey2008-02-10
* Major revision: use of Function, including some non-structural onesGravatar letouzey2008-02-10
* Major revision of FSetAVL: more Function, including some non-structural onesGravatar letouzey2008-02-09
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
* misc improvementsGravatar letouzey2008-02-08
* better comments in FMapInterfaceGravatar letouzey2008-02-08
* better comments in FSetInterfaceGravatar letouzey2008-02-08
* Change implementation of resolution for typeclasses to use a customizedGravatar msozeau2008-02-08
* more complete FSets.vGravatar letouzey2008-02-08
* one forgotten compatibility lemmaGravatar letouzey2008-02-08
* Fix obligations not being discharged due to new definition of complement.Gravatar msozeau2008-02-06
* New algorithm to resolve morphisms, after discussion with NicolasGravatar msozeau2008-02-06
* kill some useless module aliases E:=X (for better name printing, see Elie's 1...Gravatar letouzey2008-02-05
* Add Morphisms for Qceiling and QfloorGravatar roconnor2008-02-05
* Reorganization of FSet+FMap : no more files specific to Weak Sets/MapsGravatar letouzey2008-02-04
* Add new files theories/Program/Basics.v and theories/Classes/Relations.vGravatar msozeau2008-02-03
* factorization part II (Properties + EqProperties), inclusion of FSetDecide (f...Gravatar letouzey2008-02-02
* Thanks to Elie, we can share duplicated stuff in FSets: for a start, FSetWeak...Gravatar letouzey2008-02-01
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
* Support for occurences and 'in' in class_setoid, work on corresponding tactic...Gravatar msozeau2008-01-30
* Nicer proofs.Gravatar roconnor2008-01-24
* remove Fourier Failure warnings.Gravatar roconnor2008-01-24
* Prove the decidability of arithmetical statements using the real numbers.Gravatar roconnor2008-01-24