aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
* Fixing #3896 (incorrect sigma given to printer).Gravatar Hugo Herbelin2015-01-03
* A global [gfail] tactic which works like [fail] except that it fails even if ...Gravatar Arnaud Spiwack2014-12-23
* Remove compatibility layer from Ltac's [fail].Gravatar Arnaud Spiwack2014-12-23
* Fix compilation error in some configurations.Gravatar Arnaud Spiwack2014-12-23
* Add a backtracking version of Ltac's [match].Gravatar Arnaud Spiwack2014-12-19
* Fixed bad newlines in output for std output and emacs.Gravatar Pierre Courtieu2014-12-18
* Fixing bug #3796.Gravatar Pierre-Marie Pédrot2014-12-17
* Fixing CAMLP4 compilation.Gravatar Pierre-Marie Pédrot2014-12-16
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 00:37:43 +0000