aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
* adding an option functional_induction_rewrite_dependent to make functional in...Gravatar jforest2009-12-16
* Improved strategy for rewriting lemma possibly depending because of evars.Gravatar herbelin2009-12-14
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Completion of r12580 (better rendering of dependent rewrite and inversion).Gravatar herbelin2009-12-13
* Revision 12557 continued (better rendering of dependent rewrite)Gravatar herbelin2009-12-13
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* Improved the rendering of "dependent rewrite" and hence of "inversion"Gravatar herbelin2009-12-12
* Turn evars created by a tactic application into a subgoal immediately inGravatar msozeau2009-12-06
* Fix anomaly when using typeclass resolution with filtered hyps in evars.Gravatar msozeau2009-12-06
* Restored rewriting of JMeq using JMeq_rect and co when the domains are the sameGravatar herbelin2009-12-03
* Fix make_exact_entry to allow applying [forall x, P x] hints directly,Gravatar msozeau2009-12-01
* Fix bug in typeclass resolution. Better handling of universes inGravatar msozeau2009-12-01
* Fix backtracking heuristic in typeclass resolution. Gravatar msozeau2009-11-30
* Substitute terms for evars-as-goals as soon as they are solved inGravatar msozeau2009-11-27
* Minor fixes in typeclasses, avoiding repeated evar normalizations.Gravatar msozeau2009-11-24
* Lazier behaviour of [auto] when introducing hypothesis: query the hint db's o...Gravatar puech2009-11-21
* Addendum to revision 12501.Gravatar herbelin2009-11-12
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Backtracking on the use of automatically generated schemes forGravatar herbelin2009-11-11
* Compatibility ocaml <= 3.09Gravatar herbelin2009-11-10
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Quick fix for restoring a left-to-right rewriting lemma compatibleGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* - Fix discharge bug in typeclasses: some constrs were not actuallyGravatar msozeau2009-11-06
* Misc fixes.Gravatar msozeau2009-11-06
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Clarification in commentsGravatar glondu2009-10-28
* Remove old compatibility stuff (Tacred.nf)Gravatar glondu2009-10-28
* Make usage of Dyn explicitGravatar glondu2009-10-28
* Backport fix for indexing of sorts which collapse every Type occurrenceGravatar msozeau2009-10-28
* Fixes around typeclasses:Gravatar msozeau2009-10-27
* fix previous commitGravatar corbinea2009-10-27
* fixed czar bug with parametric inductivesGravatar corbinea2009-10-27
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-04 12:24:45 +0000