aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* 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
* Keep the Z_scope local to this file.Gravatar roconnor2008-01-24
* Changing R to a local definition so that it isn't exported.Gravatar roconnor2008-01-23
* TypoGravatar notin2008-01-23
* Adding Zdiv_le_compat_lGravatar thery2008-01-22
* Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...Gravatar msozeau2008-01-18
* Change notation for setoid inequality, coerce objects before comparing them. ...Gravatar msozeau2008-01-18
* Fix Makefile bug, using .v instead of .vo and document SetoidDec.vGravatar msozeau2008-01-17
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Bug in sqrt321Gravatar thery2008-01-17
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Remove spurious .d, better tactics.Gravatar msozeau2008-01-07
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* more user-friendly versions of some properties lemmas in FSets/FMapGravatar letouzey2008-01-04
* Add partial setoids in theories/Classes, add SetoidDec class for setoids with...Gravatar msozeau2008-01-04
* Implicit arguments in class field declarationsGravatar msozeau2008-01-02
* Better resolution of implicit parameters in typeclass binders, add extensiona...Gravatar msozeau2008-01-02
* Move Classes.Setoid to Classes.SetoidClass to avoid name clash.Gravatar msozeau2007-12-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Pour éviter des erreus lors de make doc dues à du code source non taggé en...Gravatar notin2007-12-21
* Deux petits théorèmes utiles dans Minus.vGravatar notin2007-12-21
* Quelques arguments en plus...Gravatar glondu2007-12-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 12:21:14 +0000