aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
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
2009-12-30Fixing bug #2146 (broken selection of occurrences in "change").herbelin
2009-12-29Improving descend_in_conjunctions (using a combinators instead of a tactic)herbelin
2009-12-28Safer, though ad hoc, approach to re-interpretation of the argument ofherbelin
2009-12-27Fix "Existing Instance" to handle globality information and "Existingmsozeau
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2009-12-24Opened the possibility to type Ltac patterns but it is not fully functional yetherbelin
2009-12-23Moved a bit further the code for pattern interpretation in match goalherbelin
2009-12-21Generic support for open terms in tacticsherbelin
2009-12-19Backtrack on making exact hints for lemmas starting with productsmsozeau
2009-12-16adding an option functional_induction_rewrite_dependent to make functional in...jforest
2009-12-14Improved strategy for rewriting lemma possibly depending because of evars.herbelin
2009-12-13Made the side-conditions of lemmas always come last when chaining "apply in"herbelin
2009-12-13Completion of r12580 (better rendering of dependent rewrite and inversion).herbelin
2009-12-13Revision 12557 continued (better rendering of dependent rewrite)herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-22 00:47:44 +0000