aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-25Merge PR #13447: Remove unused parsing codecoqbot-app[bot]
2020-11-25Merge PR #13228: [micromega] Performance of liaPierre-Marie Pédrot
2020-11-25Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bugcoqbot-app[bot]
2020-11-25Merge PR #13405: Alternative implementation of the Micromega persistent cacheVincent Laporte
2020-11-25Merge PR #13343: Update syntax in auto.rst chaptercoqbot-app[bot]
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-24Add a changelog.Pierre-Marie Pédrot
2020-11-24Keep accessed objects in memory in Persistent_cache.Pierre-Marie Pédrot
2020-11-24Regenerate the csdp cache for the test-suite.Pierre-Marie Pédrot
2020-11-24Alternative implementation of the Micromega persistent cache.Pierre-Marie Pédrot
2020-11-24Preserve sharing in the Micromega cache.Pierre-Marie Pédrot
2020-11-24Add an explicit signature to the MakeCache functor in Micromega.Pierre-Marie Pédrot
2020-11-24Merge PR #13436: Fixes #13432: typo in #11172 causing notations mentioning a ...coqbot-app[bot]
2020-11-24Fixing [dup] and [swap]Cyril Cohen
2020-11-24Merge PR #13466: Fix linter: incorrect commit was picked in CIcoqbot-app[bot]
2020-11-24Merge PR #13455: Fix comparison of extracted array literalscoqbot-app[bot]
2020-11-24Merge PR #13444: Fixes another instance of bug #7967 and #8076: restriction o...coqbot-app[bot]
2020-11-24Merge PR #13420: Modular printing algorithm for bench/render_results.coqbot-app[bot]
2020-11-24Merge PR #13411: Rename the confusing neutral annotation in CClosure.coqbot-app[bot]
2020-11-24Fix linter: incorrect commit was picked in CIGaëtan Gilbert
2020-11-23Add COPYALL and APPENDALL edit ops, drop unneeded codeJim Fehrle
2020-11-23Fix comparison of extracted array literalsGaëtan Gilbert
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notat...coqbot-app[bot]
2020-11-23Merge PR #13446: Adding debugging printer for stacks on EConstrPierre-Marie Pédrot
2020-11-23Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneousl...Pierre-Marie Pédrot
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make s...coqbot-app[bot]
2020-11-22Remove unused parsing codeJim Fehrle
2020-11-22Adding debugging printer for stacks of EConstr.Hugo Herbelin
2020-11-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-22Uniformizing indentation in ppvernac.ml.Hugo Herbelin
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
2020-11-22Fixes another instance of bug #7967: restriction of universes in "Context".Hugo Herbelin
2020-11-22Fix timeout by ensuring signal exceptions are not erroneously caughtLasse Blaauwbroek
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the sam...Pierre-Marie Pédrot
2020-11-21Merge PR #13431: Make sure accumulators do not exceed the minor heap (partly ...coqbot-app[bot]
2020-11-21Fixes #13432: regression with notations involving coercions caused by #11172.Hugo Herbelin
2020-11-21Remove dependency on BinNat.Guillaume Melquiond
2020-11-21Rename the confusing neutral annotation in CClosure.Pierre-Marie Pédrot
2020-11-20Merge PR #13248: Build all_stdlib.v in test suite makefilecoqbot-app[bot]
2020-11-20Merge PR #13265: Add support for general non-necessarily-recursive binders in...coqbot-app[bot]
2020-11-20Merge PR #13352: Configure default value of -native-compilercoqbot-app[bot]
2020-11-20Add a testcase.Guillaume Melquiond
2020-11-20Add changelog for #13265.Hugo Herbelin
2020-11-20Tests for notations with general single (non-recursive) binders.Hugo Herbelin
2020-11-20Documentation of the support for general single binders in notations.Hugo Herbelin
2020-11-20Merge PR #13233: add perennial to benchmark suitePierre-Marie Pédrot
2020-11-20Enforcing when a binding variable has no explicit type in constr_notation.Hugo Herbelin
2020-11-20A step towards supporting pattern cast deeplier.Hugo Herbelin
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 06:01:35 +0000