index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
Fix incorrect caching of local hints w.r.t sections
Matthieu Sozeau
2016-06-16
*
Compat with ocaml 4.01
Matthieu Sozeau
2016-06-16
*
Fix iterative deepening strategy failing too early
Matthieu Sozeau
2016-06-16
*
Implement limited proof search and iterative deepening.
Matthieu Sozeau
2016-06-16
*
Typeclasses eauto based on new proof engine,
Matthieu Sozeau
2016-06-16
*
A stronger invariant on the syntax of TacAssert, what allows for a
Hugo Herbelin
2016-06-16
*
Merge 'pr/191' into trunk
Enrico Tassi
2016-06-16
|
\
*
\
Merge PR #100: fresh now accepts more things than just identifiers.
Pierre-Marie Pédrot
2016-06-16
|
\
\
|
|
*
Goal selectors are now tacticals and can be used as such.
Cyprien Mangin
2016-06-14
|
|
/
|
/
|
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-13
|
\
\
|
*
|
Fixing a try with in apply that has become too weak in 8.5.
Hugo Herbelin
2016-06-11
*
|
|
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-09
|
*
|
Improve the interpretation scope of arguments of an ltac match.
Hugo Herbelin
2016-06-09
*
|
|
Fixing #4787 (Unset Bracketing Last Introduction Pattern not working).
Hugo Herbelin
2016-06-07
*
|
|
Removing the Q_constr file.
Pierre-Marie Pédrot
2016-06-05
*
|
|
Moving Hipattern to a regular ML file.
Pierre-Marie Pédrot
2016-06-05
*
|
|
Removing PATTERN uses in Hipattern.
Pierre-Marie Pédrot
2016-06-05
*
|
|
Add a synonymous Set Debug Typeclasses for Set Typeclasses Debug, for uniform...
Hugo Herbelin
2016-06-02
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
|
|
|
*
|
Revert "Rename Lexer -> CLexer."
Pierre-Marie Pédrot
2016-05-31
*
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
*
|
Fix bug #4746: Anomaly: Evar ?X10 was not declared.
Pierre-Marie Pédrot
2016-05-29
|
*
|
rewrite/Univs: Fix bug # 4498.
Matthieu Sozeau
2016-05-26
|
*
|
Hints/Univs: fix bug #4628 anomalies
Matthieu Sozeau
2016-05-23
*
|
|
Removing some compatibility layers in Tactics.
Pierre-Marie Pédrot
2016-05-17
*
|
|
Removing the old refine tactic from the Tactics module.
Pierre-Marie Pédrot
2016-05-17
*
|
|
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 "exact_constr" 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
|
*
|
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
2016-05-09
*
|
|
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 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
*
|
|
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
*
|
|
Moving Ftactic and Geninterp to the engine folder.
Pierre-Marie Pédrot
2016-05-04
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
|
*
|
In Regular Subst Tactic mode, ensure that the order of hypotheses is
Hugo Herbelin
2016-05-03
|
*
|
Fix bug #4707: clearbody much slower in 8.5pl1.
Pierre-Marie Pédrot
2016-05-03
*
|
|
Revert "In the short term, stronger invariant on the syntax of TacAssert, what"
Hugo Herbelin
2016-04-27
[next]