aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Adding the destauto tactic, that reduces match by destructing matchedGravatar courtieu2010-07-22
* Fix for bug #2350 was really too quick. Here is a version that works better.Gravatar herbelin2010-07-21
* Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).Gravatar herbelin2010-07-21
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Be more clever when trying to find out the relation inGravatar msozeau2010-07-15
* Finish adding out-of-the-box support for camlp4Gravatar letouzey2010-07-09
* Fix generalize_eqs tactic to not consider defined variables as being generali...Gravatar msozeau2010-06-30
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Made "replace" accepts open terms on its left-hand-side.Gravatar herbelin2010-06-28
* Fixed a bug introduced in a combination in r12807 and revealed inGravatar herbelin2010-06-28
* Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).Gravatar herbelin2010-06-22
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
* Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).Gravatar herbelin2010-06-13
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
* Made intros_until and onInductionArg a bit stricter and robustGravatar herbelin2010-06-13
* Fixed a bug in pretty-printing "induction" and "destruct" due to aGravatar herbelin2010-06-13
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 07:48:26 +0000