index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
tactics.mllib
Age
Commit message (
Expand
)
Author
2014-03-03
Removing Termdn, and putting the relevant code in Btermdn. The current Termdn
Pierre-Marie Pédrot
2013-11-25
Remove the Hiddentac module.
Arnaud Spiwack
2013-11-14
Implementation of Ltac's match and match goal fully based on IStream.
aspiwack
2013-11-10
Centralizing the Ltac-defining functions in Tacenv.
ppedrot
2013-11-10
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
ppedrot
2013-11-09
Revert the previous commit. It broke Coq compilation.
ppedrot
2013-11-09
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
ppedrot
2013-11-02
A whole new implemenation of the refine tactic.
aspiwack
2013-06-21
Splitted up Genarg in four different levels:
ppedrot
2013-06-12
Moving coercion functions out of Tacinterp.
ppedrot
2013-05-09
Removing unused module Nbtermdn.
ppedrot
2012-10-16
Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp
letouzey
2012-05-29
No need to have Refine amongst Hightactics.cm*a
letouzey
2012-03-30
Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl
letouzey
2010-04-22
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-03-05
Add a generic tactic option builder. Use it in firstorder to set the
msozeau
2009-12-13
Made the side-conditions of lemmas always come last when chaining "apply in"
herbelin
2009-11-08
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-04-24
Fixing bug #2308 ("instantiate" tactic did not comply with
herbelin
2009-03-20
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
