index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
ltac
/
tacinterp.ml
Age
Commit message (
Expand
)
Author
2016-06-03
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-02
Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.
Hugo Herbelin
2016-05-31
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-16
Put the "change" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
Put the "generalize" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
Put the "cofix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
Put the "exact" family of tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
Put the "fix" tactic in the monad.
Pierre-Marie Pédrot
2016-05-09
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-04
Normalizing the names of dynamic types to follow a typ_* scheme.
Pierre-Marie Pédrot
2016-05-04
Removing useless generic arguments.
Pierre-Marie Pédrot
2016-05-04
Interpretation function can return any untyped value.
Pierre-Marie Pédrot
2016-05-04
Removing external uses of Val.inject and making Geninterp.interp return Val.t
Pierre-Marie Pédrot
2016-05-04
Removing the Value.of_* API for parameterized types.
Pierre-Marie Pédrot
2016-05-04
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
Simplifying the code of Tacinterp.
Pierre-Marie Pédrot
2016-05-04
Getting rid of the Geninterp.generic_interp function.
Pierre-Marie Pédrot
2016-05-04
Switching to an untyped toplevel representation for Ltac values.
Pierre-Marie Pédrot
2016-04-27
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-11
Removing the ad-hoc tactic_expr type.
Pierre-Marie Pédrot
2016-04-08
Fixing printing of toplevel values.
Pierre-Marie Pédrot
2016-03-25
Moving type_uconstr to Pretyping.
Pierre-Marie Pédrot
2016-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
