aboutsummaryrefslogtreecommitdiff
path: root/test-suite
AgeCommit message (Expand)Author
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
2020-11-16Merge PR #13380: Fixing the "IllTypedInstance" anomaly part of #5512coqbot-app[bot]
2020-11-16Merge PR #12690: Mini-fix of Locate for recursive notations using named varia...coqbot-app[bot]
2020-11-16Avoid exposing an internal names when "intros _ H" fails.Hugo Herbelin
2020-11-16Merge PR #13373: Fixes #13363: in pose_all_metas_as_evars, use the context of...coqbot-app[bot]
2020-11-16Merge PR #13387: Fixes #12348: de Bruijn indices bug in the imitation part of...coqbot-app[bot]
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
2020-11-16Merge PR #12685: Propagating scope information in indirect application to a r...Pierre-Marie Pédrot
2020-11-16Fix test-suite.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
2020-11-16Fixing the "IllTypedInstance" anomaly part of #5512.Hugo Herbelin
2020-11-16Merge PR #13290: Grant #13278: computation of return predicate takes care of ...coqbot-app[bot]
2020-11-15Ensuring the body of the notation in Locate is printed at level 0.Hugo Herbelin
2020-11-15Adding support for Locate "( x , y )".Hugo Herbelin
2020-11-15Fixing Locate for recursive notations with names.Hugo Herbelin
2020-11-15Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block verbati...Li-yao Xia
2020-11-15Fixes #12348: long-standing de Bruijn indices bug in imitation (solve_simple_...Hugo Herbelin
2020-11-15Merge PR #13383: Fixes #11816: using {wf ...} in a local fixpoint is an error...coqbot-app[bot]
2020-11-15Merge PR #13376: Fixes #13266: Avoiding encapsulating exceptions w/o a handle...coqbot-app[bot]
2020-11-15Adding an output test to check that the hint commands respect their locality.Pierre-Marie Pédrot
2020-11-15Fixes #11816: using {wf ...} in a local fixpoint is an error, not an anomaly.Hugo Herbelin
2020-11-15Default disable automatic generalization of Instance typeGaëtan Gilbert
2020-11-15Propagating scope information in indirect application to a reference.Hugo Herbelin
2020-11-15Merge PR #13339: In -noinit mode, add support for Proof using, using is not a...Pierre-Marie Pédrot
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
2020-11-14Coqdoc: we move a newline at a better place.Hugo Herbelin
2020-11-14Addressing #13304: how to verbatim an expression mentioning >>.Hugo Herbelin
2020-11-14Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.Hugo Herbelin
2020-11-13Fixes #13363: case of a meta not paying attention to being under binders.Hugo Herbelin
2020-11-13Fix incorrect "avoid" set in globenv extra dataGaëtan Gilbert
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-12Test case for Proof using in -noinit mode.Théo Zimmermann
2020-11-12Merge PR #13359: Print failed test suite logs in CIcoqbot-app[bot]
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...coqbot-app[bot]
2020-11-12Print failed test suite logs in CIGaëtan Gilbert
2020-11-12Add the test as a misc script.Pierre-Marie Pédrot
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
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-10Fix running unit tests with dune compiled coqGaëtan Gilbert
2020-11-10Merge PR #13325: [compat] remove 8.10coqbot-app[bot]
2020-11-09[obligation] Proper handle no obligations on `Next Obligation`Emilio Jesus Gallego Arias
2020-11-09[compat] remove 8.10Enrico Tassi
2020-11-09Merge PR #13217: Addresses #13216: use of type classes in the return clause o...Pierre-Marie Pédrot
2020-11-08fixupCyril 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-05Regression tests for the various combinations of mixed terms and binders in n...Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 10:15:49 +0000