coq

coq copied to clipboard

Ltac profile: automatically adapt printing width

2

Using Printing Width to get the max printing width. Close #18438

SkySkimmer

Fix #5342 This makes `destruct` and `Scheme` use the same error message as `match`.

SkySkimmer

Declare global sort variables

7

This PR adds new vernacular instructions `Sort q1 ... qn.` / `Sorts q1 ... qn.` to declare global fresh sort qualities `q1`, ..., `qn`. Its intended usage is to add...

kyoDralliam

[ci] Resurrect CI job for OCaml trunk.

74

Depends on a few patches still.

ejgallego

#### Description of the problem A few tactics which do not strictly refine the goal lose the name of the goal. E.g.: ```coq Goal exists x, x = 0. unshelve...

herbelin

Names given with "Arguments" are not used when splitting a record in tactic mode

1

#### Description of the problem ```coq Record T := { f : Type -> Type }. Arguments f _ A. Goal T. split; intro. (* returns "X : Type |-...

herbelin

Ltac2 should provide a better API for manually managing the context

2

Currently it's not possible to write efficient Coq in Ltac2 without making use of terms with unbound references, which are incompatible with tactics like `cbv` and `match!` without `Constr.in_context`, which...

JasonGross

#### Description of the problem Hi, I've just noticed a problem with `Reset` (which is a great feature for testing while writing code!). Basically, as you see below, I can...

pierrevial

Ltac2: rewrite with local hypothesis does not work

5

#### Description of the problem In the following example (from CUDW2023) rewriting with a local hypothesis does not work using Ltac2 rewrite: ``` Require Import Reals. Require Import QArith. Require...

MSoegtropIMC

Anomaly "in retyping: Variable H unbound." (with ssr apply)

2

#### Description of the problem ```coq From Coq Require Import ssreflect. Goal True -> True. move=> H. apply: (H) {H}. (* Error: Anomaly "in retyping: Variable H unbound." *) ```...

aedoq