aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-12Print failed test suite logs in CIGaëtan Gilbert
2020-11-12Merge the Linked and LinkedInteractive constructors.Pierre-Marie Pédrot
2020-11-12Statically ensure that the native interactive flag is always set to true.Pierre-Marie Pédrot
2020-11-12Statically ensure that native update locations are of form Linked*.Pierre-Marie Pédrot
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-12Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -Icoqbot-app[bot]
2020-11-12Add the test as a misc script.Pierre-Marie Pédrot
2020-11-12Add documentation about the soundness bug.Pierre-Marie Pédrot
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
2020-11-12Fix Iris CI scriptGaëtan Gilbert
2020-11-12Add changelog for #13345.Hugo Herbelin
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
2020-11-11Add changelog for #13351.Hugo Herbelin
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-10Merge PR #13335: Fix running unit tests with dune compiled coqcoqbot-app[bot]
2020-11-10Merge PR #13315: Convert logic chapter to prodncoqbot-app[bot]
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-10Fix running unit tests with dune compiled coqGaëtan Gilbert
2020-11-10Merge PR #13325: [compat] remove 8.10coqbot-app[bot]
2020-11-10Merge PR #13322: [obligation] Properly handle no obligations on `Next Obligat...coqbot-app[bot]
2020-11-10Merge PR #13297: Remove the native symbol registering from the safe environment.coqbot-app[bot]
2020-11-09Add additional escape sequences for notationsJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-09Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml...coqbot-app[bot]
2020-11-09Merge PR #13327: Fix documentation of Ltac ::=coqbot-app[bot]
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
2020-11-09Remove virtually unused replace rule.Théo Zimmermann
2020-11-09Fix #5226: Add index entry for ::=.Théo Zimmermann
2020-11-09Fix indentation of todo in Ltac chapter.Théo Zimmermann
2020-11-09Remove the native symbol registering from the safe environment.Pierre-Marie Pédrot
2020-11-09[compat] remove 8.10Enrico Tassi
2020-11-09Merge PR #13310: Fix macOS CI on Azure.coqbot-app[bot]
2020-11-09Merge PR #13217: Addresses #13216: use of type classes in the return clause o...Pierre-Marie Pédrot
2020-11-09Merge PR #13173: Lint stdlib with -mangle-names #4coqbot-app[bot]
2020-11-08fixupCyril Cohen
2020-11-06Merge PR #13139: Clean the constr-as-hint APIcoqbot-app[bot]
2020-11-06Update doc/changelog/06-ssreflect/13317-ssr_dup_swap_apply_ipat.rstCyril Cohen
2020-11-06Merge PR #13255: Fixes #13244: support for coercions in Searchcoqbot-app[bot]
2020-11-06Merge PR #13284: Fixing interpretation of rewrite_strat argument in LtacPierre-Marie Pédrot
2020-11-06Intro pattern extensions for dup, swap and applyCyril Cohen
2020-11-06The "( X in t )" hack used in the syntax of ssr rewrite may be only parsing.Hugo Herbelin
2020-11-05Merge PR #12099: More parsing/printing notation/abbreviation consistency for ...Emilio Jesus Gallego Arias
2020-11-05Merge PR #12797: [refman] Take large chunks out of the tactics chapter.coqbot-app[bot]
2020-11-05Added change log for #12099.Hugo Herbelin
2020-11-05Minor cut elimination in the code of constrintern.ml.Hugo Herbelin
2020-11-05Regression tests for the various combinations of mixed terms and binders in n...Hugo Herbelin
2020-11-05Accept local variables in mixed terms and binders of notations.Hugo Herbelin
2020-11-05Accept section variables in notations with mixed terms and binders.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:17:59 +0000