aboutsummaryrefslogtreecommitdiff
path: root/tactics/hightactics.mllib
AgeCommit message (Expand)Author
2016-03-21Creating a dedicated ltac/ folder for Hightactics.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 the tactic related code from Metasyntax to a new file.Pierre-Marie Pédrot
2016-03-20Moving Tacinterp to Hightactics.Pierre-Marie Pédrot
2016-03-17Removing the special status of generic arguments defined by Coq itself.Pierre-Marie Pédrot
2016-03-06Moving Autorewrite to Hightatctic.Pierre-Marie Pédrot
2016-03-06Moving Eauto to a simple ML file.Pierre-Marie Pédrot
2015-12-24Removing auto from the tactic AST.Pierre-Marie Pédrot
2014-05-16Moving argument-free tactics out of the AST into a dedicatedPierre-Marie Pédrot
2014-03-26Adding an interface to Eqdecide and putting the grammar rules in a dedicatedPierre-Marie Pédrot
2013-10-04Splitting Class_tactics between code and CAMLP4/5 declarations.ppedrot
2013-09-26Splitting Rewrite into a code part and a CAMLP4-dependent one.ppedrot
2012-05-29No need to have Refine amongst Hightactics.cm*aletouzey
2009-04-07Move setoid_rewrite to its own module and do some clean up inmsozeau
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:17:02 +0000