index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
/
tacsubst.ml
Commit message (
Expand
)
Author
Age
*
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-09-21
*
Moving Ltac-specific generic arguments to their own file in the ltac/ folder.
Pierre-Marie Pédrot
2016-09-15
*
Exporting a generic argument induction_arg. As a consequence,
Hugo Herbelin
2016-06-18
*
Adding eintros to respect the e- prefix policy.
Hugo Herbelin
2016-06-18
*
Fixing missing substitution / printing cases of TacSelect.
Pierre-Marie Pédrot
2016-06-16
*
A stronger invariant on the syntax of TacAssert, what allows for a
Hugo Herbelin
2016-06-16
*
Removing "rename" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "exact" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "intro" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Removing "double induction" from the tactic AST.
Pierre-Marie Pédrot
2016-06-03
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Removing useless generic arguments.
Pierre-Marie Pédrot
2016-05-04
*
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
Hugo Herbelin
2016-04-27
*
In the short term, stronger invariant on the syntax of TacAssert, what
Hugo Herbelin
2016-04-27
*
Attempt to slightly improve abusive "Collision between bound
Hugo Herbelin
2016-04-27
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
Pierre-Marie Pédrot
Hugo Herbelin
Emilio Jesus Gallego Arias