aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-08Merge PR #10318: Test goal range in "only" selectorsPierre-Marie Pédrot
2019-06-08Merge PR #10263: [proofs] Remove unused API [detected by coverage]Pierre-Marie Pédrot
2019-06-08Fix #10339: Anomaly in Ltac2.Pierre-Marie Pédrot
2019-06-08[Test-suite] Add non-regression test case for #8725Vincent Laporte
2019-06-08Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.Hugo Herbelin
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
2019-06-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...Pierre-Marie Pédrot
2019-06-08Updated changelog.Hugo Herbelin
2019-06-08Mini fix documentation coqtop in passing.Hugo Herbelin
2019-06-08Documenting new options -require-import, -require-export, etc.Hugo Herbelin
2019-06-08Command line: adding variants for Require, aligning on the vernac syntax.Hugo Herbelin
2019-06-07Merge PR #10236: Update coqdev-setup-proofgeneral for duneEmilio Jesus Gallego Arias
2019-06-07Merge PR #10330: Dune: run coqc with -w +defaultEmilio Jesus Gallego Arias
2019-06-07Merge PR #10335: simple IO CI branch is now `master`Emilio Jesus Gallego Arias
2019-06-07Merge PR #10311: Ltac2 codeowner / changelogMaxime Dénès
2019-06-07simple IO CI branch is now `master`Gaëtan Gilbert
2019-06-07Merge PR #10308: Merge the two sources of monomorphic constraints for side-ef...Gaëtan Gilbert
2019-06-07test suite: don't try to coqchk failed testsGaëtan Gilbert
2019-06-07Update changelog for 103032 and 10305Enrico Tassi
2019-06-07Dune: run coqc with -w +defaultGaëtan Gilbert
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-07Fix bug #5710Claude Stolze
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Merge PR #10304: Clean up tuto0 and tuto1 to use better practices and explain...Pierre-Marie Pédrot
2019-06-06Merge PR #10278: vernac_load doesn't get a ?proof argumentEmilio Jesus Gallego Arias
2019-06-06Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.Vincent Laporte
2019-06-06Doc for per commit compile lintGaëtan Gilbert
2019-06-06CI: Test ml compilation of each commit in a PR in lint jobGaëtan Gilbert
2019-06-06Merge PR #10323: Remove old overlaysEmilio Jesus Gallego Arias
2019-06-06Merge the two sources of monomorphic constraints for side-effects.Pierre-Marie Pédrot
2019-06-06Merge PR #10299: Lazy substitution of section contexts in opaque proofsMaxime Dénès
2019-06-06Fix panel behavior as requested by #10292Claude Stolze
2019-06-06Remove old overlaysGaëtan Gilbert
2019-06-06Update changes.rst as a follow-up to #9743Kazuhiko Sakaguchi
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-06Clean, document, and expand plugin tutorials 0 and 1Talia Ringer
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06Merge PR #10305: Fix SSR (un)fold of polymorphic terms - issue 9336Enrico Tassi
2019-06-06Merge PR #10302: Fix SSR 'case B:b' with universe polymorphic equalityEnrico Tassi
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-05Add Andreas Lynge to CREDITSAndreas Lynge
2019-06-05Remove redundancies in the INSTALL doc.Théo Zimmermann
2019-06-05Changelog entry for Ltac2 (missing from #10002).Théo Zimmermann
2019-06-05Add codeowner for Ltac2. Forgotten in #10002.Théo Zimmermann
2019-06-05Fix #10283: clearer dependency documentation for building CoqIDE.Théo Zimmermann
2019-06-05vernac_load doesn't get a ?proof argumentGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 02:35:49 +0000