index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
/
tacinterp.ml
Commit message (
Expand
)
Author
Age
*
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
Hugo Herbelin
2016-04-27
*
Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"
Hugo Herbelin
2016-04-27
*
Revert "Passing around the precedence to the generic printer so as to solve"
Hugo Herbelin
2016-04-27
*
Revert "When interpreting "match goal with ... end" in ltac, expand evars by"
Hugo Herbelin
2016-04-27
*
Revert "Fixing space in an error message."
Hugo Herbelin
2016-04-27
*
Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...
Hugo Herbelin
2016-04-27
*
Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"
Hugo Herbelin
2016-04-27
*
Fixing space in an error message.
Hugo Herbelin
2016-04-27
*
When interpreting "match goal with ... end" in ltac, expand evars by
Hugo Herbelin
2016-04-27
*
Passing around the precedence to the generic printer so as to solve
Hugo Herbelin
2016-04-27
*
Honor parsing and printing levels for tactic entry in TACTIC EXTEND and
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
*
Removing the ad-hoc tactic_expr type.
Pierre-Marie Pédrot
2016-04-11
*
Fixing printing of toplevel values.
Pierre-Marie Pédrot
2016-04-08
*
Moving type_uconstr to Pretyping.
Pierre-Marie Pédrot
2016-03-25
*
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-21
Hugo Herbelin
Pierre-Marie Pédrot