aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Morphisms.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
* Allow interactive editing of {C,}Morphisms in PGGravatar Jason Gross2017-04-28
* Typeclasses: use once in by clause for typeclass eautoGravatar Matthieu Sozeau2016-06-28
* setoid_rewrite: fix the Params resolution tacticGravatar Matthieu Sozeau2016-06-16
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-22 01:36:53 +0000