aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Morphisms.v
Commit message (Expand)AuthorAge
* 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
* Bug squashing day !Gravatar msozeau2008-04-17
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
* Fixes in new Morphisms files. Gravatar msozeau2008-04-09
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* Minor fixes. Use expanded type in class_tactics for Morphism search, toGravatar msozeau2008-04-02
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Fix test-suite files, change conflicting notation "->rel" and the othersGravatar msozeau2008-03-29
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* 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
* Implementation of rewriting under lambdas. Tested on exists only.Gravatar msozeau2008-03-18
* Correct implementation of normalization of signatures using setoidGravatar msozeau2008-03-18
* Add the possibility of specifying constants to unfold for typeclassGravatar msozeau2008-03-17
* Removed unneeded tactics from RelationClasses. UseGravatar msozeau2008-03-16
* Using the "relation" constant made some unifications fail in the newGravatar msozeau2008-03-16
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* Minor fixes on setoid rewriting. Now uses definitions of [relation] andGravatar msozeau2008-03-16
* Add a missing morphism declaration that turns morphisms on R ==> R' toGravatar msozeau2008-03-09
* Coquille vraisemblablement introduite par la révision 10628Gravatar notin2008-03-06
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Fix compilation problem (hopefully).Gravatar msozeau2008-02-28
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* Backtrack changes on eauto, move specialized version of eauto inGravatar msozeau2008-02-14
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
* New algorithm to resolve morphisms, after discussion with NicolasGravatar msozeau2008-02-06