index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
ltac
/
g_ltac.ml4
Age
Commit message (
Expand
)
Author
2016-06-17
par: like all: but in parallel
Enrico Tassi
2016-06-16
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-14
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-06
STM: proof block detection for par:
Enrico Tassi
2016-06-06
STM: proof block detection/error resilience API
Enrico Tassi
2016-06-05
Adding the Print Ltac Signature command.
Pierre-Marie Pédrot
2016-05-31
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-10
Removing the Entry module now that rules need not be marshalled.
Pierre-Marie Pédrot
2016-05-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-04-27
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-24
Higher-level API for tactic notations.
Pierre-Marie Pédrot
2016-04-14
Moving and enhancing the grammar_tactic_prod_item_expr type.
Pierre-Marie Pédrot
2016-04-09
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-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
