aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* More fallout from elisp renameGravatar Anders Kaseorg2014-10-16
* Relaxing again the test on types of replacements in tactic changeGravatar Hugo Herbelin2014-10-16
* In convert_concl/convert_hyp: nf_enter -> enter.Gravatar Hugo Herbelin2014-10-16
* Revert "Naming main goal "Main""Gravatar Hugo Herbelin2014-10-16
* Refactoring proofview: make the definition of the logic monad polymorphic.Gravatar Arnaud Spiwack2014-10-16
* Refresh to avoid algebraic universes on the right.Gravatar Matthieu Sozeau2014-10-16
* Fix test-suite scripts.Gravatar Matthieu Sozeau2014-10-16
* Bug fixed by Hugo.Gravatar Matthieu Sozeau2014-10-16
* Grab Existential Variables: restore the goal order from v8.4.Gravatar Arnaud Spiwack2014-10-16
* Proofview: cleanup: no more reference to Goal.goal.Gravatar Arnaud Spiwack2014-10-16
* Put evars remaining after a tactic on the shelf.Gravatar Arnaud Spiwack2014-10-16
* Refine: proper scoping of the future goals.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove [advance] from the API.Gravatar Arnaud Spiwack2014-10-16
* Proofview: remove unused [refresh_sigma] compatibility primitive.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove some functions from the compatibility layer.Gravatar Arnaud Spiwack2014-10-16
* Goal: remove most of the API (make [Goal.goal] concrete).Gravatar Arnaud Spiwack2014-10-16
* Make [Goal.goal] be exactly [Evar.t].Gravatar Arnaud Spiwack2014-10-16
* Goal: remove dead code.Gravatar Arnaud Spiwack2014-10-16
* Expose Proofview.Refine.with_type in the API.Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: remove the handle type, and simplify the API.Gravatar Arnaud Spiwack2014-10-16
* Move the handling of the principal evar from refine to evd.Gravatar Arnaud Spiwack2014-10-16
* Move the handling a new evars from the [Proofview.Refine] module to [Evd].Gravatar Arnaud Spiwack2014-10-16
* Evd: a few comments to document the increasingly wide internal [evar_map] type.Gravatar Arnaud Spiwack2014-10-16
* Evd: remove/update obsolete comments.Gravatar Arnaud Spiwack2014-10-16
* Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Gravatar Arnaud Spiwack2014-10-16
* Proofview: small optimisation/simplification.Gravatar Arnaud Spiwack2014-10-16
* ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Gravatar Arnaud Spiwack2014-10-16
* Adding a timeout to bug #2447.Gravatar Pierre-Marie Pédrot2014-10-15
* To stay closer to non-primitive projections, only unfold primitiveGravatar Matthieu Sozeau2014-10-15
* Make use of unfolded primitive projections when elaborating match on aGravatar Matthieu Sozeau2014-10-15
* Fix ill-typed debugging functionGravatar Matthieu Sozeau2014-10-15
* Fix for bug #3618.Gravatar Matthieu Sozeau2014-10-15
* Remaining tactics of the Auto module were put in the monad.Gravatar Pierre-Marie Pédrot2014-10-15
* Closed bug 3710.Gravatar Matthieu Sozeau2014-10-15
* Bug 3692 is fixed.Gravatar Matthieu Sozeau2014-10-15
* Bug 3628 is fixed.Gravatar Matthieu Sozeau2014-10-15
* Fix test-suite files which failed due to usage of $(admit)$ whichGravatar Matthieu Sozeau2014-10-15
* Fix bug 3637.Gravatar Matthieu Sozeau2014-10-15
* Reenable FO unification of primitive projections and their eta-expandedGravatar Matthieu Sozeau2014-10-15
* Fix test-suite file after moving back to using C as the nameGravatar Matthieu Sozeau2014-10-15
* Modify the heuristic for unfolding lhs or rhs in evarconv, consideringGravatar Matthieu Sozeau2014-10-15
* Implement a different strategy to expand primitive projections only whenGravatar Matthieu Sozeau2014-10-15
* Add an option to not print primitive projection parameters, which canGravatar Matthieu Sozeau2014-10-15
* Fix -async-proofs-always-delegate (close 3740)Gravatar Enrico Tassi2014-10-15
* Fix ML paths (thanks Jean-Marc Notin for bisecting it)Gravatar Enrico Tassi2014-10-14
* Revert "Move eta-expansion after delta reduction in kernel reduction. This ma...Gravatar Matthieu Sozeau2014-10-14
* Oops, forgot a fix needed after the rebase.Gravatar Matthieu Sozeau2014-10-14
* Fix bug #3698: stack overflow due to eta+canonical structures inGravatar Matthieu Sozeau2014-10-14
* Fix typo, thanks Mike Shulman for spotting itGravatar Enrico Tassi2014-10-13
* Fixing "change" and "fold" after convert_hyp/convert_concl moved toGravatar Hugo Herbelin2014-10-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 01:18:30 +0000