index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
tacenv.mli
Age
Commit message (
Expand
)
Author
2015-05-15
Granting wish #4048: Locate Ltac prints the source of redefined Ltac.
Pierre-Marie Pédrot
2015-05-11
Adding a test to check whether two tactic notations conflict.
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-12-16
Fixing CAMLP4 compilation.
Pierre-Marie Pédrot
2014-10-01
Fixing nice printing of error reporting with ml tactics bound to ltac names.
Hugo Herbelin
2014-08-31
Getting rid of atomic tactics in Tacenv.
Pierre-Marie Pédrot
2014-08-31
Moving code of tactic interpretation from Tacenv to Vernacentries.
Pierre-Marie Pédrot
2014-08-18
Moving the TacExtend node from atomic to plain tactics.
Pierre-Marie Pédrot
2014-07-27
Qualified ML tactic names. The plugin name is used to discriminate
Pierre-Marie Pédrot
2014-06-30
Useless keeping of dirpath in tactic aliases.
Pierre-Marie Pédrot
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
