index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
/
g_ltac.ml4
Commit message (
Expand
)
Author
Age
*
par: like all: but in parallel
Enrico Tassi
2016-06-17
*
Typo in comment.
Hugo Herbelin
2016-06-16
*
Fixing parsing of constr argument of ltac functions at level 8 in the
Hugo Herbelin
2016-06-16
*
Merge 'pr/191' into trunk
Enrico Tassi
2016-06-16
|
\
|
*
Ident selectors cannot be used inside an Ltac expression.
Cyprien Mangin
2016-06-14
|
*
Goal selectors are now tacticals and can be used as such.
Cyprien Mangin
2016-06-14
|
*
Remove the need for brackets in goal selectors.
Cyprien Mangin
2016-06-14
|
*
Fix usage of Pervasives in goal selectors.
Cyprien Mangin
2016-06-14
|
*
Fix the pretty-printing of goal range selectors.
Cyprien Mangin
2016-06-14
|
*
Add goal range selectors.
Cyprien Mangin
2016-06-14
*
|
STM: proof block detection for par:
Enrico Tassi
2016-06-06
*
|
STM: proof block detection/error resilience API
Enrico Tassi
2016-06-06
|
/
*
Adding the Print Ltac Signature command.
Pierre-Marie Pédrot
2016-06-05
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Removing the Entry module now that rules need not be marshalled.
Pierre-Marie Pédrot
2016-05-10
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"
Hugo Herbelin
2016-04-27
*
Revert "Typo in comment."
Hugo Herbelin
2016-04-27
*
Typo in comment.
Hugo Herbelin
2016-04-27
*
Fixing parsing of constr argument of ltac functions at level 8 in the
Hugo Herbelin
2016-04-27
*
Higher-level API for tactic notations.
Pierre-Marie Pédrot
2016-04-24
*
Moving and enhancing the grammar_tactic_prod_item_expr type.
Pierre-Marie Pédrot
2016-04-14
*
Removing extra spaces in printing arguments of VERNAC EXTEND.
Hugo Herbelin
2016-04-09
*
Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...
Hugo Herbelin
2016-04-09
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21