aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Fix bug #2317: setoid_rewrite ignored binding lists. SlightlyGravatar msozeau2010-06-09
* Relaxed the freshness constraint in "intro H" (with "H" explicit):Gravatar herbelin2010-06-09
* Tentative fix for typeclass resolution raising Evd.define exceptions.Gravatar msozeau2010-06-08
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Avoid computing tactic printing tree (std_ppcmds) when printing not needed inGravatar herbelin2010-06-03
* New pass on inductive schemesGravatar herbelin2010-05-29
* Fixing Derive Inversion for new proof engineGravatar herbelin2010-05-26
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* term matching in ltac was not coherent with match goal in presence of wildcar...Gravatar jforest2010-05-06
* Fix discrimination of sorts which doesn't play well with cumulativityGravatar msozeau2010-05-02
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)Gravatar herbelin2010-04-20
* Fixed some printing bugs.Gravatar herbelin2010-04-18
* Solved a few problems of auto by bypassing the call to apply.Gravatar herbelin2010-04-17
* Use nice "unfold" instead of ugly "change" to display calls to unfold hintsGravatar herbelin2010-04-17
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
* Removing redundant internal variants of apply tactic and simplification of ML...Gravatar herbelin2010-04-14
* Improving compatibility between 8.2 and 8.3Gravatar herbelin2010-04-05
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* Applied greenrd's patch to fix bug 2255 (injection failed toGravatar herbelin2010-03-27
* Fix splitting evars tactics and stop dropping evar constraints whenGravatar msozeau2010-03-15
* fixed confusion between number of cstr arguments and number of pattern variab...Gravatar barras2010-03-12
* Fix lifting of constraints in generalized rewriting tactic.Gravatar msozeau2010-03-07
* Fixes in rewrite and a Elimination/Case to Scheme:Gravatar msozeau2010-03-06
* Improvements in generalized rewriting:Gravatar msozeau2010-03-05
* Fix [autounfold] to accept general [in] clauses.Gravatar msozeau2010-03-05
* Add a generic tactic option builder. Use it in firstorder to set theGravatar msozeau2010-03-05
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* Support for generalized rewriting under dependent binders, using theGravatar msozeau2010-01-26
* Quick fix for references to section variables unbound in the currentGravatar msozeau2010-01-26
* New version of 12650 that was broken (supporting again records whenGravatar herbelin2010-01-12
* Added module sharing support for typeclasses and hints (pri_auto_tactic).Gravatar soubiran2010-01-12
* revert commit 12650 for the moment, since it breaks MSetAVLGravatar letouzey2010-01-12
* Temporary fix to compensate the loss of descent on dependentGravatar herbelin2010-01-12
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* Improving descend_in_conjunctions (using a combinators instead of a tactic)Gravatar herbelin2009-12-29
* Safer, though ad hoc, approach to re-interpretation of the argument ofGravatar herbelin2009-12-28
* Fix "Existing Instance" to handle globality information and "ExistingGravatar msozeau2009-12-27
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Opened the possibility to type Ltac patterns but it is not fully functional yetGravatar herbelin2009-12-24
* Moved a bit further the code for pattern interpretation in match goalGravatar herbelin2009-12-23
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* Backtrack on making exact hints for lemmas starting with productsGravatar msozeau2009-12-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 13:08:30 +0000