index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
ltac
Commit message (
Expand
)
Author
Age
...
|
|
|
|
*
Add is_ind, is_constructor, is_proj
Jason Gross
2016-06-07
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
About printing of traces of failures while calling ltac code.
Hugo Herbelin
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-06
|
|
/
/
|
/
|
|
|
*
|
Make Ltac Profiling an setting
Jason Gross
2016-06-05
|
*
|
Synchronize the profiler state with the document
Jason Gross
2016-06-05
|
*
|
LtacProf for Coq trunk
Jason Gross
2016-06-05
|
*
|
Strip some trailing spaces
Jason Gross
2016-06-05
|
/
/
*
|
Adding the Print Ltac Signature command.
Pierre-Marie Pédrot
2016-06-05
*
|
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
*
|
Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.
Hugo Herbelin
2016-06-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
|
Put the "move" tactic in the monad.
Pierre-Marie Pédrot
2016-05-17
*
|
Put the "change" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
Put the "specialize_eq" tactic in the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
Put the "generalize dependent" 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 "*_cast_no_check" tactics 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-16
*
|
Put the "clear" tactic into the monad.
Pierre-Marie Pédrot
2016-05-16
*
|
Generate more user-readable tactic notation kernel names.
Pierre-Marie Pédrot
2016-05-16
*
|
Making the grammar command extend API purely functional.
Pierre-Marie Pédrot
2016-05-11
*
|
Moving the constr empty entry registering to the state-based API.
Pierre-Marie Pédrot
2016-05-11
*
|
Turning the grammar extend command API into a state-passing one.
Pierre-Marie Pédrot
2016-05-11
*
|
Moving the grammar summary to Pcoq.
Pierre-Marie Pédrot
2016-05-11
*
|
AlistNsep token now accepts an arbitrary separator.
Pierre-Marie Pédrot
2016-05-10
*
|
Removing the Entry module now that rules need not be marshalled.
Pierre-Marie Pédrot
2016-05-10
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
*
|
Pass user symbol to tactic notation printers.
Pierre-Marie Pédrot
2016-05-08
*
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
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
*
|
Do not generate generic arguments for data which only requires toplevel values.
Pierre-Marie Pédrot
2016-05-04
*
|
More toplevel value representation sharing.
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-05-04
*
|
Generate parsing rules for ML tactics in the same order as before a7917a32.
Pierre-Marie Pédrot
2016-05-02
*
|
Useless code in Tacentries.
Pierre-Marie Pédrot
2016-05-02
*
|
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
Hugo Herbelin
2016-04-27
[prev]
[next]
Jason Gross
Hugo Herbelin
Enrico Tassi
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias