aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Morphisms.v
Commit message (Expand)AuthorAge
* 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
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Various bug fixes in type classes and subtac:Gravatar msozeau2008-07-01
* Enhanced discrimination nets implementation, which can now work withGravatar msozeau2008-06-27
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* - Correct handling of DependentMorphism error, using tclFAIL instead ofGravatar msozeau2008-06-10
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Backtrack commit 10887 (priorité des notations pour les signatures deGravatar notin2008-05-05
* It seems more natural to put those operators at same level as "->"...Gravatar glondu2008-05-05
* Debug implementation of failing tactics in Morphism to allow earlierGravatar msozeau2008-04-26
* - Fix bug in eterm which was not taking filtered contexts in evars intoGravatar msozeau2008-04-25
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
* - Correct unification for the rewrite variant of setoid_rewrite,Gravatar msozeau2008-04-21