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
*
* removed declare_constant and declare_internal_constant
vsiles
2010-09-02
*
Improved printing of Unfoldable constants in hints databases (used
herbelin
2010-09-02
*
Export printing functions for extra arguments. Maybe there's a way to
msozeau
2010-08-03
*
Capitulation wrt "change pat with term": instead of solving the
herbelin
2010-07-30
*
Fix bug #2209, don't use the fragile argument name "y" to pass the
msozeau
2010-07-28
*
oops. commited files I shouldn't have. reverting on r13341
barras
2010-07-28
*
ported r13340 to trunk
barras
2010-07-28
*
Minor fixes:
msozeau
2010-07-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).
herbelin
2010-07-22
*
Adding the destauto tactic, that reduces match by destructing matched
courtieu
2010-07-22
*
Fix for bug #2350 was really too quick. Here is a version that works better.
herbelin
2010-07-21
*
Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).
herbelin
2010-07-21
*
Reverted 13293 commited mistakenly. Sorry for the noise.
herbelin
2010-07-18
*
Tentative de suppression de l'import automatique des hints et coercions.
herbelin
2010-07-18
*
Be more clever when trying to find out the relation in
msozeau
2010-07-15
*
Finish adding out-of-the-box support for camlp4
letouzey
2010-07-09
*
Fix generalize_eqs tactic to not consider defined variables as being generali...
msozeau
2010-06-30
*
Made tclABSTRACT normalize evars before saying it does not support
herbelin
2010-06-29
*
Made "replace" accepts open terms on its left-hand-side.
herbelin
2010-06-28
*
Fixed a bug introduced in a combination in r12807 and revealed in
herbelin
2010-06-28
*
Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).
herbelin
2010-06-22
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Fixed commit 13125 (stricter check of induction args): an interpretation
herbelin
2010-06-14
*
Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).
herbelin
2010-06-13
*
Fixed bug #2314 (inversion using not checking the correctness of its arguments
herbelin
2010-06-13
*
Made intros_until and onInductionArg a bit stricter and robust
herbelin
2010-06-13
*
Fixed a bug in pretty-printing "induction" and "destruct" due to a
herbelin
2010-06-13
*
Fixed bug #2135 (second-order unification was raising cryptic message)
herbelin
2010-06-12
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Fix bug #2317: setoid_rewrite ignored binding lists. Slightly
msozeau
2010-06-09
*
Relaxed the freshness constraint in "intro H" (with "H" explicit):
herbelin
2010-06-09
*
Tentative fix for typeclass resolution raising Evd.define exceptions.
msozeau
2010-06-08
*
Added support for Ltac-matching terms with variables bound in the pattern
herbelin
2010-06-06
*
Avoid computing tactic printing tree (std_ppcmds) when printing not needed in
herbelin
2010-06-03
*
New pass on inductive schemes
herbelin
2010-05-29
*
Fixing Derive Inversion for new proof engine
herbelin
2010-05-26
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
Remove compile-command pragmas for emacs
letouzey
2010-05-19
*
Applicative commutative cuts in Fixpoint guard condition
pboutill
2010-05-18
*
Improved the efficiency of evars traverals thanks to a split of
herbelin
2010-05-13
*
term matching in ltac was not coherent with match goal in presence of wildcar...
jforest
2010-05-06
*
Fix discrimination of sorts which doesn't play well with cumulativity
msozeau
2010-05-02
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)
herbelin
2010-04-20
*
Fixed some printing bugs.
herbelin
2010-04-18
*
Solved a few problems of auto by bypassing the call to apply.
herbelin
2010-04-17
[next]