aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Morphisms.v
Commit message (Expand)AuthorAge
* Move Params definition in generalize rewriting out of a section so thatGravatar Matthieu Sozeau2014-06-29
* 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
* 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
* 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
* 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
* Proper fix for complement/flip instances.Gravatar msozeau2011-10-10
* Fix bug #2557 and an issue with Propers for complementGravatar msozeau2011-10-07
* Avoid registering λ and Π as keywords just for some private Local NotationGravatar letouzey2011-09-06
* Merge branch 'subclasses' into coq-trunkGravatar msozeau2011-05-05
* - Allow rewriting under abitrary products, not just those in Prop.Gravatar msozeau2011-02-28
* f_equiv : a clone of f_equal that handles setoid equivalencesGravatar letouzey2011-01-04
* Numbers: some improvements in proofsGravatar letouzey2011-01-03
* Fixed commit r13359 which was incomplete for its "trunk" part. ThanksGravatar herbelin2010-07-31
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Support for generalized rewriting under dependent binders, using theGravatar msozeau2010-01-26
* Support "Local Obligation Tactic" (now the default in sections).Gravatar msozeau2010-01-11
* Rename proper to proper_prf to avoid clash with CoRN, Gravatar msozeau2009-12-03
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Fix new instances that could easily make class resolution loop on Gravatar msozeau2009-10-22
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* 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
* Do a fixpoint on the result of typeclass search to force theGravatar msozeau2009-06-08
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* Minor fixes in typeclasses:Gravatar msozeau2009-05-16
* Improvements in typeclasses eauto and generalized rewriting:Gravatar msozeau2009-05-05
* Fixes for bugs in r12110:Gravatar msozeau2009-04-28
* - Implementation of a new typeclasses eauto procedure based on successGravatar msozeau2009-04-27
* Rename [Morphism] into [Proper] and [respect] into [proper] to complyGravatar msozeau2009-04-21
* Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact thatGravatar msozeau2009-04-20
* Only export the notations of Morphism as well as Equivalence throughGravatar msozeau2009-04-17
* Rewrite of setoid_rewrite to modularize it based on proof-producingGravatar msozeau2009-04-13
* Fix [subrelation] clauses that privileged the weakest. Better impl argsGravatar msozeau2009-02-04
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Fix handling of [inverse] in setoid_rewrite, with an hopefully completeGravatar msozeau2008-12-08
* Use manual implicts in Classes and rationalize class parameter names.Gravatar msozeau2008-09-14
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 02:13:55 +0000