aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* 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
* Extend the syntax of simpl with a delta flag.Gravatar Arnaud Spiwack2014-12-12
* In discrimination nets, do not index lambdas if they're part of a betaGravatar Matthieu Sozeau2014-12-12
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Fix dummy argument use in guess_elim: there are some cases where X_indGravatar Matthieu Sozeau2014-12-10
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.Gravatar Hugo Herbelin2014-12-08
* Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Gravatar Arnaud Spiwack2014-12-08
* Step 4 : atomize_thenGravatar Hugo Herbelin2014-12-07
* Step 2Gravatar Hugo Herbelin2014-12-07
* Step 1Gravatar Hugo Herbelin2014-12-07
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* Exporting store of goals so that new_evar in convert, intro, etc. canGravatar Hugo Herbelin2014-12-07
* For compatibility purpose, when setoid_rewriting a hypothesis, beta-iotaGravatar Pierre-Marie Pédrot2014-12-02
* More invariants in the code of Rewrite.Gravatar Pierre-Marie Pédrot2014-12-01
* Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ...Gravatar Hugo Herbelin2014-11-30
* Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.Gravatar Hugo Herbelin2014-11-30
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 19:02:52 +0000