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
...
*
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
*
Use nice "unfold" instead of ugly "change" to display calls to unfold hints
herbelin
2010-04-17
*
Util: remove list_split_at which is a clone of list_chop
letouzey
2010-04-16
*
Removing redundant internal variants of apply tactic and simplification of ML...
herbelin
2010-04-14
*
Improving compatibility between 8.2 and 8.3
herbelin
2010-04-05
*
Added a function in typing.ml to solve evars of a constr w/o going back down ...
herbelin
2010-04-05
*
Applied greenrd's patch to fix bug 2255 (injection failed to
herbelin
2010-03-27
*
Fix splitting evars tactics and stop dropping evar constraints when
msozeau
2010-03-15
*
fixed confusion between number of cstr arguments and number of pattern variab...
barras
2010-03-12
[prev]
[next]