aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.mllib
AgeCommit message (Expand)Author
2020-06-04Move the Cbn module to tactics/.Pierre-Marie Pédrot
2020-04-21[declare] [tactics] Move declare to `vernac`Emilio Jesus Gallego Arias
2020-04-15[proofs] Move pfedit to `proofs`Emilio Jesus Gallego Arias
2020-04-15[proof] Merge `Proof_global` into `Declare`Emilio Jesus Gallego Arias
2020-04-15[proof] Move proof_global functionality to Proof_global from PfeditEmilio Jesus Gallego Arias
2019-10-30[declare] Remove declare_scheme hook in DeclareEmilio Jesus Gallego Arias
2019-08-27[declare] Move proof_entry type to declare, put interactive proof data on top...Emilio Jesus Gallego Arias
2019-06-24Move Declare to tactics folder.Pierre-Marie Pédrot
2018-12-11[api] Move reduction modules to `tactics`Emilio Jesus Gallego Arias
2018-10-30Move abstract out of tactics.mlGaëtan Gilbert
2016-09-15Moving Tactic_matching to ltac/ folder.Pierre-Marie Pédrot
2016-08-19Moving Taccoerce to ltac/ folder.Pierre-Marie Pédrot
2016-05-04Moving Ftactic and Geninterp to the engine folder.Pierre-Marie Pédrot
2016-03-25Moving Autorewrite back to tactics/.Pierre-Marie Pédrot
2016-03-25Moving Eqdecide to tactics/.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
2016-03-20Moving Tacsubst to hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tacenv to Hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tactic_debug to Hightactic.Pierre-Marie Pédrot
2016-03-20Moving Tacintern to Hightactics.Pierre-Marie Pédrot
2016-03-20Moving Tacinterp to Hightactics.Pierre-Marie Pédrot
2016-03-06Moving Autorewrite to Hightatctic.Pierre-Marie Pédrot
2016-03-06Putting Tactic_debug just below Tacinterp.Pierre-Marie Pédrot
2016-03-06Moving Tactic_debug to tactics/ folder.Pierre-Marie Pédrot
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-10-01Made Tacsubst independent of Auto at linking time so that Tacenv doesHugo Herbelin
2014-09-05Adding a Ftactic module for potentially focussing tactics.Pierre-Marie Pédrot
2014-09-03Useless hooks in Tacintern.Pierre-Marie Pédrot
2014-05-08Moving Dnet-related code to tactics/.Pierre-Marie Pédrot
2014-03-03Removing Termdn, and putting the relevant code in Btermdn. The current TermdnPierre-Marie Pédrot
2013-11-25Remove the Hiddentac module.Arnaud Spiwack
2013-11-14Implementation of Ltac's match and match goal fully based on IStream.aspiwack
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-02A whole new implemenation of the refine tactic.aspiwack
2013-06-21Splitted up Genarg in four different levels:ppedrot
2013-06-12Moving coercion functions out of Tacinterp.ppedrot
2013-05-09Removing unused module Nbtermdn.ppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-05-29No need to have Refine amongst Hightactics.cm*aletouzey
2012-03-30Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconclletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-03-05Add a generic tactic option builder. Use it in firstorder to set themsozeau
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-04-24Fixing bug #2308 ("instantiate" tactic did not comply withherbelin
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:12 +0000