aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Fix unescaped end-of-lines (OCaml warning 29)Gravatar glondu2010-09-13
* Improving a few error messages in Ltac interpretationGravatar herbelin2010-09-11
* * removed declare_constant and declare_internal_constant Gravatar vsiles2010-09-02
* Improved printing of Unfoldable constants in hints databases (usedGravatar herbelin2010-09-02
* Export printing functions for extra arguments. Maybe there's a way toGravatar msozeau2010-08-03
* Capitulation wrt "change pat with term": instead of solving theGravatar herbelin2010-07-30
* Fix bug #2209, don't use the fragile argument name "y" to pass theGravatar msozeau2010-07-28
* oops. commited files I shouldn't have. reverting on r13341Gravatar barras2010-07-28
* ported r13340 to trunkGravatar barras2010-07-28
* Minor fixes:Gravatar msozeau2010-07-27
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 13:06:20 +0000