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
2016-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-02
Separation of concern in TacAlias API.
Pierre-Marie Pédrot
2015-12-21
Using dynamic values in tactic evaluation.
Pierre-Marie Pédrot
2015-06-01
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-15
Granting wish #4048: Locate Ltac prints the source of redefined Ltac.
Pierre-Marie Pédrot
2015-05-15
Merge v8.5 into trunk
Hugo Herbelin
2015-05-11
Adding a test to check whether two tactic notations conflict.
Pierre-Marie Pédrot
2015-01-23
Splitting ML tactics in one function per grammar entry.
Pierre-Marie Pédrot
2015-01-21
Embedding the index of the ML tactic entry in the Tacexpr AST.
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
