aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.mllib
Commit message (Expand)AuthorAge
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Made Tacsubst independent of Auto at linking time so that Tacenv doesGravatar Hugo Herbelin2014-10-01
* Adding a Ftactic module for potentially focussing tactics.Gravatar Pierre-Marie Pédrot2014-09-05
* Useless hooks in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
* Moving Dnet-related code to tactics/.Gravatar Pierre-Marie Pédrot2014-05-08
* Removing Termdn, and putting the relevant code in Btermdn. The current TermdnGravatar Pierre-Marie Pédrot2014-03-03
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
* Implementation of Ltac's match and match goal fully based on IStream.Gravatar aspiwack2013-11-14
* Centralizing the Ltac-defining functions in Tacenv.Gravatar ppedrot2013-11-10
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Revert the previous commit. It broke Coq compilation.Gravatar ppedrot2013-11-09
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-09
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Moving coercion functions out of Tacinterp.Gravatar ppedrot2013-06-12
* Removing unused module Nbtermdn.Gravatar ppedrot2013-05-09
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* No need to have Refine amongst Hightactics.cm*aGravatar letouzey2012-05-29
* Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclGravatar letouzey2012-03-30
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Add a generic tactic option builder. Use it in firstorder to set theGravatar msozeau2010-03-05
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 21:53:13 +0000