aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactic_option.ml
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
* Use a Summary.ref for the tactic in tactic options for proper backtrackingGravatar msozeau2013-06-05
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Minor fixes:Gravatar msozeau2010-07-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Add a generic tactic option builder. Use it in firstorder to set theGravatar msozeau2010-03-05