aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes
Commit message (Expand)AuthorAge
* Fix #4978: priorities of Equivalence instancesGravatar Matthieu Sozeau2016-08-17
* Typeclasses: use once in by clause for typeclass eautoGravatar Matthieu Sozeau2016-06-28
* setoid_rewrite: fix the Params resolution tacticGravatar Matthieu Sozeau2016-06-16
* Typeclasses: stdlib fixes for new search algorithmGravatar Matthieu Sozeau2016-06-16
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * Fix handling of arity of definitional classes.Gravatar Matthieu Sozeau2016-03-24
* | Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Put implicits back as in 8.4.Gravatar Matthieu Sozeau2015-12-31
* Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
* Univs: add Strict Universe Declaration option (on by default)Gravatar Matthieu Sozeau2015-10-07
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
* Mark PreOrder as a consequence of Equivalence. (Fix bug #4213)Gravatar Guillaume Melquiond2015-05-12
* Fix instances of universe-polymorphic generalized rewriting to avoidGravatar Matthieu Sozeau2015-04-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 20:24:18 +0000