aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-10-16Make [Goal.goal] be exactly [Evar.t].Arnaud Spiwack
2014-10-16Goal: remove dead code.Arnaud Spiwack
2014-10-16Expose Proofview.Refine.with_type in the API.Arnaud Spiwack
2014-10-16Proofview.Refine: remove the handle type, and simplify the API.Arnaud Spiwack
2014-10-16Move the handling of the principal evar from refine to evd.Arnaud Spiwack
2014-10-16Move the handling a new evars from the [Proofview.Refine] module to [Evd].Arnaud Spiwack
2014-10-16Evd: a few comments to document the increasingly wide internal [evar_map] type.Arnaud Spiwack
2014-10-16Evd: remove/update obsolete comments.Arnaud Spiwack
2014-10-16Proofview.Refine: delay the marking of new evars as goals from [new_evar] to ...Arnaud Spiwack
2014-10-16Proofview: small optimisation/simplification.Arnaud Spiwack
2014-10-16ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Arnaud Spiwack
2014-10-15Adding a timeout to bug #2447.Pierre-Marie Pédrot
2014-10-15To stay closer to non-primitive projections, only unfold primitiveMatthieu Sozeau
2014-10-15Make use of unfolded primitive projections when elaborating match on aMatthieu Sozeau
2014-10-15Fix ill-typed debugging functionMatthieu Sozeau
2014-10-15Fix for bug #3618.Matthieu Sozeau
2014-10-15Remaining tactics of the Auto module were put in the monad.Pierre-Marie Pédrot
2014-10-15Closed bug 3710.Matthieu Sozeau
2014-10-15Bug 3692 is fixed.Matthieu Sozeau
2014-10-15Bug 3628 is fixed.Matthieu Sozeau
2014-10-15Fix test-suite files which failed due to usage of $(admit)$ whichMatthieu Sozeau
2014-10-15Fix bug 3637.Matthieu Sozeau
2014-10-15Reenable FO unification of primitive projections and their eta-expandedMatthieu Sozeau
2014-10-15Fix test-suite file after moving back to using C as the nameMatthieu Sozeau
2014-10-15Modify the heuristic for unfolding lhs or rhs in evarconv, consideringMatthieu Sozeau
2014-10-15Implement a different strategy to expand primitive projections only whenMatthieu Sozeau
2014-10-15Add an option to not print primitive projection parameters, which canMatthieu Sozeau
2014-10-15Fix -async-proofs-always-delegate (close 3740)Enrico Tassi
2014-10-14Fix ML paths (thanks Jean-Marc Notin for bisecting it)Enrico Tassi
2014-10-14Revert "Move eta-expansion after delta reduction in kernel reduction. This ma...Matthieu Sozeau
2014-10-14Oops, forgot a fix needed after the rebase.Matthieu Sozeau
2014-10-14Fix bug #3698: stack overflow due to eta+canonical structures inMatthieu Sozeau
2014-10-13Fix typo, thanks Mike Shulman for spotting itEnrico Tassi
2014-10-13Fixing "change" and "fold" after convert_hyp/convert_concl moved toHugo Herbelin
2014-10-13Add support for deactivating type class inference from induction/destruct.Hugo Herbelin
2014-10-13Adding a tactic which fails if one of the goals under focus is dependent in a...Hugo Herbelin
2014-10-13Adding printers for ppproofview.Hugo Herbelin
2014-10-13Naming main goal "Main"Hugo Herbelin
2014-10-13Moving function about locs in locusops.Hugo Herbelin
2014-10-13English typo in a function name of evarconv.Hugo Herbelin
2014-10-13Added support for several impossible cases in compilation of "match".Hugo Herbelin
2014-10-13Stm: more precise representation of nested proofsEnrico Tassi
2014-10-13When loading libraries, feed back dependencies.Carst Tankink
2014-10-13Emit a warning for void Arguments statement (Close 3713)Enrico Tassi
2014-10-13Parsing of "?[" as two tokens (makes ssr compile).Enrico Tassi
2014-10-13STM: primitives to snapshot a .vi while in interactive modeEnrico Tassi
2014-10-13selective join/export of the safe_environmentEnrico Tassi
2014-10-13TQueue: new primitive to take a snapshot of the queueEnrico Tassi
2014-10-13STM: simplify how the term part of a side effect is retrievedEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 10:46:29 +0000