aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/SetoidTactics.v
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-01-24Make `Instance` without a body always open a proof.Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-06-26Export the right modules in Setoid, avoiding anomalies in generalized rewriting.Matthieu Sozeau
2012-08-08Updating headers.herbelin
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-15Stop using [obligation_tactic] from Program.Tactics as the defaultmsozeau
2009-09-08Fix the bug-ridden code used to choose leibniz or generalizedmsozeau
2009-04-21Rename [Morphism] into [Proper] and [respect] into [proper] to complymsozeau
2009-04-18Just export RelationClasses for [Equivalence] through Setoid.msozeau
2009-04-17Only export the notations of Morphism as well as Equivalence throughmsozeau
2008-12-14Generalized binding syntax overhaul: only two new binders: `() and `{},msozeau
2008-11-05Minor fixes:msozeau
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-06-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-04-20Work on the "occurrences" tactic argument. It is now possible to passmsozeau
2008-04-15Document CHANGES in setoid rewrite, move DefaultRelation tomsozeau
2008-04-12Document the new setoid rewrite tactic, and fix a few things whilemsozeau
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-22Compatibility fixes, backtrack on definitions of reflexive,msozeau
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-03-16Reorganize Program and Classes theories. Requiring Setoid no longer setsmsozeau
2008-03-08Fix bugs that were reopened due to the change of setoidmsozeau
2008-03-06Syntax changes in typeclasses, remove "?" for usual implicit argumentsmsozeau
2008-02-26Proper implicit arguments handling for assumptionsmsozeau
2008-02-06New algorithm to resolve morphisms, after discussion with Nicolasmsozeau
2008-02-03Add new files theories/Program/Basics.v and theories/Classes/Relations.vmsozeau
2008-01-17Fix Makefile bug, using .v instead of .vo and document SetoidDec.vmsozeau
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2008-01-05Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...msozeau
2007-12-31Move Classes.Setoid to Classes.SetoidClass to avoid name clash.msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau