aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/SetoidTactics.v
Commit message (Expand)AuthorAge
* 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
* Export the right modules in Setoid, avoiding anomalies in generalized rewriting.Gravatar Matthieu Sozeau2014-06-26
* Updating headers.Gravatar herbelin2012-08-08
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* 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
* Stop using [obligation_tactic] from Program.Tactics as the defaultGravatar msozeau2009-09-15
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Rename [Morphism] into [Proper] and [respect] into [proper] to complyGravatar msozeau2009-04-21
* Just export RelationClasses for [Equivalence] through Setoid.Gravatar msozeau2009-04-18
* Only export the notations of Morphism as well as Equivalence throughGravatar msozeau2009-04-17
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Minor fixes:Gravatar msozeau2008-11-05
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
* Document the new setoid rewrite tactic, and fix a few things whileGravatar msozeau2008-04-12
* - 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
* 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
* 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
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* New algorithm to resolve morphisms, after discussion with NicolasGravatar msozeau2008-02-06
* Add new files theories/Program/Basics.v and theories/Classes/Relations.vGravatar msozeau2008-02-03
* Fix Makefile bug, using .v instead of .vo and document SetoidDec.vGravatar msozeau2008-01-17
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* Move Classes.Setoid to Classes.SetoidClass to avoid name clash.Gravatar msozeau2007-12-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31