aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Equivalence.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Fix #4978: priorities of Equivalence instancesGravatar Matthieu Sozeau2016-08-17
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* 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
* Final part of moving Program code inside the main code. Adapted add_definitio...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
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix compilation errors due to last commit.Gravatar msozeau2009-09-15
* Stop using [obligation_tactic] from Program.Tactics as the defaultGravatar msozeau2009-09-15
* Just export RelationClasses for [Equivalence] through Setoid.Gravatar msozeau2009-04-18
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Minor fixes:Gravatar msozeau2008-11-05
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Use manual implicts in Classes and rationalize class parameter names.Gravatar msozeau2008-09-14
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* More compatibility fixes, revert the tauto fix that preventedGravatar msozeau2008-07-25
* New tactics [conv] to test convertibility (actually, unification) of twoGravatar msozeau2008-07-22
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Update doc and remove another overloading of equiv_*.Gravatar msozeau2008-04-14
* Renamings to avoid clashes with definitions in Relation_Definitions, nowGravatar msozeau2008-04-14
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Interpret patterns for hypotheses types in match goal in type_scope (if not aGravatar msozeau2008-03-25
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
* Compatibility fixes, backtrack on definitions of reflexive,Gravatar msozeau2008-03-22
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Correct implementation of normalization of signatures using setoidGravatar msozeau2008-03-18
* Removed unneeded tactics from RelationClasses. UseGravatar msozeau2008-03-16
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Backtrack changes on eauto, move specialized version of eauto inGravatar msozeau2008-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 21:30:49 +0000