aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Opaque implementation of auto tactics.Gravatar Pierre-Marie Pédrot2015-04-14
* Remove declarations of matched variables in change as an extension ofGravatar Matthieu Sozeau2015-04-13
* More documented representation of hint objects.Gravatar Pierre-Marie Pédrot2015-04-13
* Making the hint entry type opaque.Gravatar Pierre-Marie Pédrot2015-04-12
* Fix compilation broken by Matthieu's last commit.Gravatar Pierre Letouzey2015-04-10
* Fix #3590 for good this time, by changing the API, change's argument nowGravatar Matthieu Sozeau2015-04-10
* Eauto hints respect their priority. Fixes bug #3199.Gravatar Pierre-Marie Pédrot2015-04-10
* Making the hints for the auto tactics private.Gravatar Pierre-Marie Pédrot2015-04-10
* Fix caching of local hintdb in typeclasses eauto.Gravatar Matthieu Sozeau2015-04-09
* refresh metas in rewrite hints loaded from .vo files (fix bug #3815)Gravatar Nickolai Zeldovich2015-04-06
* Removing a probably incorrect on-the-fly require in a tactic.Gravatar Pierre-Marie Pédrot2015-04-01
* Aliasing give_up with admitGravatar Enrico Tassi2015-03-22
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Reverting r10021 which enforces early assumptions on freshness whichGravatar Hugo Herbelin2015-03-07
* Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".Gravatar Hugo Herbelin2015-03-07
* Fix bug #3590, keeping evars that are not turned into named metas byGravatar Matthieu Sozeau2015-03-03
* Removing the unused field ltacrecvars of tactic internalization.Gravatar Pierre-Marie Pédrot2015-02-27
* Hack so that refine_no_check accepts an argument which is a match on anGravatar Hugo Herbelin2015-02-27
* Somehow fixing bug #3467.Gravatar Pierre-Marie Pédrot2015-02-27
* Fixing bug #3298.Gravatar Pierre-Marie Pédrot2015-02-26
* Fixing printing of ordinals.Gravatar Pierre-Marie Pédrot2015-02-26
* [info_auto] & [info_trivial]: warning message to help users find [Info].Gravatar Arnaud Spiwack2015-02-24
* [info] tactical warning: do not suggest [info_auto] and [info_trivial].Gravatar Arnaud Spiwack2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Fixing error message when H already exists in tactic subexpression eqn:H.Gravatar Hugo Herbelin2015-02-20
* A fix for #3993 (not fully applied term to destruct when eqn is given).Gravatar Hugo Herbelin2015-02-20
* Fix bug #3938Gravatar Matthieu Sozeau2015-02-18
* Fixing bug #3944.Gravatar Pierre-Marie Pédrot2015-02-16
* Fixing bug #4016.Gravatar Pierre-Marie Pédrot2015-02-14
* Univs: fix bug #4031: wrong folding of sigma in change.Gravatar Matthieu Sozeau2015-02-12
* Fix bug #2775: Correct handling of universes in leminv.Gravatar Matthieu Sozeau2015-02-12
* Fixing compilation for 3.12.Gravatar Pierre-Marie Pédrot2015-02-12
* Tentative fix for bug #4027.Gravatar Pierre-Marie Pédrot2015-02-12
* Missing space in error messageGravatar Matěj Grabovský2015-02-11
* Fixing #4018 (uncaught exception on non-equality in intros [=]).Gravatar Hugo Herbelin2015-02-10
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Revert "Removing spurious tclWITHHOLES."Gravatar Pierre-Marie Pédrot2015-02-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Removed obsolete option "Legacy Partially Applied EliminationGravatar Hugo Herbelin2015-01-24
* Tentative workaround for bug #3798.Gravatar Pierre-Marie Pédrot2015-01-24
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"Gravatar Matthieu Sozeau2015-01-16
* Add a (by default deactivated) option to force typeclass resolution toGravatar Matthieu Sozeau2015-01-15
* Optionally allow eta-conversion during unification for type classes.Gravatar Matthieu Sozeau2015-01-15
* TCs: Properly handle Hint Extern with conclusions of the form _ -> _Gravatar Matthieu Sozeau2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing compilation of penultimate commit d08532d.Gravatar Hugo Herbelin2015-01-08
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Fix setoid rewrite.Gravatar Arnaud Spiwack2015-01-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 16:30:24 +0000