aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2010-07-22Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).herbelin
2010-07-22Adding the destauto tactic, that reduces match by destructing matchedcourtieu
2010-07-21Fix for bug #2350 was really too quick. Here is a version that works better.herbelin
2010-07-21Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).herbelin
2010-07-18Reverted 13293 commited mistakenly. Sorry for the noise.herbelin
2010-07-18Tentative de suppression de l'import automatique des hints et coercions.herbelin
2010-07-15Be more clever when trying to find out the relation inmsozeau
2010-07-09Finish adding out-of-the-box support for camlp4letouzey
2010-06-30Fix generalize_eqs tactic to not consider defined variables as being generali...msozeau
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-28Made "replace" accepts open terms on its left-hand-side.herbelin
2010-06-28Fixed a bug introduced in a combination in r12807 and revealed inherbelin
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
2010-06-13Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).herbelin
2010-06-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
2010-06-13Made intros_until and onInductionArg a bit stricter and robustherbelin
2010-06-13Fixed a bug in pretty-printing "induction" and "destruct" due to aherbelin
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-09Fix bug #2317: setoid_rewrite ignored binding lists. Slightlymsozeau
2010-06-09Relaxed the freshness constraint in "intro H" (with "H" explicit):herbelin
2010-06-08Tentative fix for typeclass resolution raising Evd.define exceptions.msozeau
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-06-03Avoid computing tactic printing tree (std_ppcmds) when printing not needed inherbelin
2010-05-29New pass on inductive schemesherbelin
2010-05-26Fixing Derive Inversion for new proof engineherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19Remove compile-command pragmas for emacsletouzey
2010-05-18Applicative commutative cuts in Fixpoint guard conditionpboutill
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-05-06term matching in ltac was not coherent with match goal in presence of wildcar...jforest
2010-05-02Fix discrimination of sorts which doesn't play well with cumulativitymsozeau
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-20Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)herbelin
2010-04-18Fixed some printing bugs.herbelin
2010-04-17Solved a few problems of auto by bypassing the call to apply.herbelin
2010-04-17Use nice "unfold" instead of ugly "change" to display calls to unfold hintsherbelin
2010-04-16Util: remove list_split_at which is a clone of list_chopletouzey
2010-04-14Removing redundant internal variants of apply tactic and simplification of ML...herbelin
2010-04-05Improving compatibility between 8.2 and 8.3herbelin
2010-04-05Added a function in typing.ml to solve evars of a constr w/o going back down ...herbelin
2010-03-27Applied greenrd's patch to fix bug 2255 (injection failed toherbelin
2010-03-15Fix splitting evars tactics and stop dropping evar constraints whenmsozeau
2010-03-12fixed confusion between number of cstr arguments and number of pattern variab...barras
2010-03-07Fix lifting of constraints in generalized rewriting tactic.msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 06:19:11 +0000