coq

coq copied to clipboard

Deprecated undocumented and unused keep/clear modifier.

10

The keep/clear modifier `>` is undocumented and **apparently unused in the whole CI** (tested by Jim in #15015). This feature does not look important enough to me to deserve a...

Zimmi48

coqtop dies with "Fatal error: exception Not_found" when Ltac Backtrace is set and the backtrace references a constant which no longer exists

1

#### Description of the problem Finished failing transaction in 18.917 secs (18.809u,0.108s) (failure) Fatal error: exception Not_found Raised at Int.Map.find in [file "clib/int.ml", line 39](https://github.com/coq/coq/blob/V8.15.0/clib/int.ml#L39), characters 14-29 Called from HMap.Make.find...

JasonGross

ssreflect `[^ ...]` pattern no longer works with name mangling since Coq 8.15

1

#### Description of the problem The following code worked fine in Coq 8.14, but no longer works in Coq 8.15: ```coq From Coq Require Import String. From Coq.ssr Require Export...

RalfJung

Command-line argument parsing for coqdoc via Arg

17

In an effort to neatly separate out argument parsing, minimize the number of globals, and create an automated help output, migrate coqdoc to use the OCaml stdlib Arg to do...

artagnon

`ltac2:(...)` in nested notations handles variable names incorrectly

1

#### Description of the problem This should work: ```coq Require Import Ltac2.Ltac2. Require Import Ltac2.Printf. Notation foo1 x := (ltac:(idtac x; exact I)) (only parsing). Notation bar1 y := (foo1...

JasonGross

See https://github.com/coq/coq/pull/16428 and #16406 , we need to add some tests that fake a global findlib install of an outdate plugin and check that Coq / coq_makefile do pick the...

ejgallego

Zify doesn't accept parametric instances of InjTyp

2

#### Description of the problem I can't add Zify support for a parametric type. I use a bitvector type `bv : N -> Type` for bitvectors of certain size (from...

tperami

Print Ltac2 Type

4

I'd like to be able to write `Print Ltac2 Type exn`

JasonGross

Ltac2 stack traces

7

#### Description of the problem I'd like to have a global setting that enables stack trace printing for Ltac2 errors. There should also be some support within the language for...

JasonGross

Uniformize semantics of :> in class after deprecation phase of #16230

17

This ends the deprecation phases of https://github.com/coq/coq/pull/16230 and https://github.com/coq/coq/pull/15802 that introduced :: instead of :> for subclasses in Class declarations. Now :> produces an error in `Class` before we can...

proux01