aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
* Remove "init" label from Termops.it_mk* specialized functionsGravatar glondu2010-09-28
* Fix bug in implementation of setoid rewriting under cases andGravatar msozeau2010-09-27
* Solving bug #2212 (unification under tuples now not allowed forGravatar herbelin2010-09-24
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't weGravatar herbelin2010-09-19
* Reverting partial fix for #2335 committed by mistake in r13435. Sorry.Gravatar herbelin2010-09-19
* Patch solving the bug but leaving open design choicesGravatar herbelin2010-09-19
* Fixed a problem introduced in r12607 after pattern_of_constr servedGravatar herbelin2010-09-17
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 01:17:33 +0000