aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes
Commit message (Expand)AuthorAge
* Remove typeclass opaque directive, some proofs in the stdlib rely on it being...Gravatar Matthieu Sozeau2015-01-15
* Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Move Params definition in generalize rewriting out of a section so thatGravatar Matthieu Sozeau2014-06-29
* Export the right modules in Setoid, avoiding anomalies in generalized rewriting.Gravatar Matthieu Sozeau2014-06-26
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Update and start testing rewrite-in-type code.Gravatar Matthieu Sozeau2014-05-09
* Restore implicit arguments of irreflexivity (fixes bug #3305).Gravatar Matthieu Sozeau2014-05-09
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Updating headers.Gravatar herbelin2012-08-08
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* Bug 2813 - Reflexive, Symmetric, Transitive instances for pointwise_relation ...Gravatar pboutill2012-06-20
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Everything compiles again.Gravatar msozeau2012-03-14
* Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...Gravatar msozeau2012-01-31
* Tentative to fix bug #2628 by not letting intuition break records. Might be t...Gravatar msozeau2012-01-28
* Added the decidability of (<=) on nat.Gravatar ppedrot2012-01-13
* Fixed the itarget of the previous commit...Gravatar ppedrot2012-01-06
* Added a typeclass-based system to reason on decidable propositions.Gravatar ppedrot2012-01-06
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Fix bug #2586 and enhance clsubst* as well as a side effectGravatar msozeau2011-10-18
* Proper fix for complement/flip instances.Gravatar msozeau2011-10-10
* Fix bug #2557 and an issue with Propers for complementGravatar msozeau2011-10-07
* Use an ad-hoc monomorphic list in RelationClasses to avoid some universe cons...Gravatar letouzey2011-10-05
* Avoid registering λ and Π as keywords just for some private Local NotationGravatar letouzey2011-09-06
* StrictOrder marked explicitly to be in PropGravatar letouzey2011-07-04
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* - Allow rewriting under abitrary products, not just those in Prop.Gravatar msozeau2011-02-28
* Add [Typeclasses Debug] option that respects backtracking, solveGravatar msozeau2011-01-11
* f_equiv : a clone of f_equal that handles setoid equivalencesGravatar letouzey2011-01-04
* Numbers: some improvements in proofsGravatar letouzey2011-01-03
* First release of Vector library.Gravatar pboutill2010-12-10
* In passing, very quick uniformization of coqdoc headers in a few files.Gravatar herbelin2010-12-09
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
* Minor fixes:Gravatar msozeau2010-07-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 20:47:09 +0000