aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2010-03-06Fixes in rewrite and a Elimination/Case to Scheme:msozeau
2010-03-05Improvements in generalized rewriting:msozeau
2010-03-05Fix [autounfold] to accept general [in] clauses.msozeau
2010-03-05Add a generic tactic option builder. Use it in firstorder to set themsozeau
2010-02-10Fix [Existing Class] impl and add documentation. Fix computation of themsozeau
2010-01-30Update CHANGES, add documentation for new commands/tactics and do a bitmsozeau
2010-01-26Support for generalized rewriting under dependent binders, using themsozeau
2010-01-26Quick fix for references to section variables unbound in the currentmsozeau
2010-01-12New version of 12650 that was broken (supporting again records whenherbelin
2010-01-12Added module sharing support for typeclasses and hints (pri_auto_tactic).soubiran
2010-01-12revert commit 12650 for the moment, since it breaks MSetAVLletouzey
2010-01-12Temporary fix to compensate the loss of descent on dependentherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 02:28:49 +0000