aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Tactics.v
Commit message (Expand)AuthorAge
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Fix bug #4923: Warning: appcontext is deprecated.Gravatar Pierre-Marie Pédrot2016-07-18
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* The "on_last_hyp" tactic now behaves as it should.Gravatar Cyprien Mangin2015-06-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Updating headers.Gravatar herbelin2012-08-08
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.Gravatar msozeau2011-06-07
* Add a flag to hide obligations in Program-generated terms under anGravatar msozeau2011-02-28
* In Program obligation, do not use auto on non-proposition goals byGravatar msozeau2011-02-17
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Correction program_simplify. Devrait corriger certaines contribs.Gravatar aspiwack2010-05-28
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Minor fixes.Gravatar msozeau2010-03-05
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
* Add [Next Obligation with tactic] support (wish #1953).Gravatar msozeau2010-01-26
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-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
* Misc fixes:Gravatar msozeau2009-09-10
* Experimental support for automatic destruction of recursive calls andGravatar msozeau2009-04-08
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
* Fix for bug #1973 provided by Brian Campbell.Gravatar msozeau2008-10-22
* Fix a bug reintroduced in [setoid_reflexivity] etc...Gravatar msozeau2008-09-09
* More debugging of [Equations], now able to discharge even the heavilyGravatar msozeau2008-09-07
* Initial implementation of a new command to define (dependent) functions byGravatar msozeau2008-09-02
* Fixes in dependent induction tactic to keep names, allow givingGravatar msozeau2008-08-21
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* Temporary fix for bug #1876, printing fails because of unresolvedGravatar msozeau2008-06-13
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Minor fixes. Use expanded type in class_tactics for Morphism search, toGravatar msozeau2008-04-02
* Improve error handling and messages for typeclasses. Gravatar msozeau2008-03-28
* Interpret patterns for hypotheses types in match goal in type_scope (if not aGravatar msozeau2008-03-25
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
* Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...Gravatar msozeau2008-01-18
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* Better resolution of implicit parameters in typeclass binders, add extensiona...Gravatar msozeau2008-01-02
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Addition of more general tactics for equality. Functional extensionality and ...Gravatar msozeau2007-10-24
* Add more equality tactics. Upgrade program_simpl for discrimination of conjun...Gravatar msozeau2007-08-26
* Move Program tactics into a proper theories/ directory as they are general pu...Gravatar msozeau2007-08-07