coq

coq copied to clipboard

Segmentation fault on S390X architecture

12

While compiling coq-elpi 1.15.6 using coq 8.16.0 on S390X, a segmentation fault occurs. The full log is [here](https://buildd.debian.org/status/fetch.php?pkg=coq-elpi&arch=s390x&ver=1.15.6-1&stamp=1662929687&raw=0) ; here is the relevant part: ``` COQC theories/wip/memoization.v Segmentation fault make[5]:...

SnarkBoojum

IDE crashed when trying to do edit->preferences

33

``` ------------------------------------- Translated Report (Full Report Below) ------------------------------------- Process: coqide.exe [7799] Path: /Applications/Coq-Platform~8.15~2022.04.app/Contents/Resources/bin/coqide.exe Identifier: coqide.exe Version: ??? Code Type: X86-64 (Native) Parent Process: launchd [1] User ID: 503 Date/Time: 2022-05-22...

richardwzp

Feature request: Set No Assumptions

6

#### Description of the feature request I would love an option to set called "No Assumptions" that causes `Defined` and `Qed` to error if the defined term is not either...

jwiegley

lia/zify fails with "Hypothesis H depends on the body of z3" if typechecking depends on Z.max being convertible to a constant

1

```coq Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. Open Scope Z_scope. Parameter foo: Z -> Prop. Definition bar(i: Z)(f1 f2: foo i): Prop. Admitted. Goal forall (f1: foo (Z.max 0 1))...

samuelgruetter

Error reporting when building stdlib has too short paths

5

- put some error in a stdlib file, eg `theories/Init/Logic.v` - dune build the error will be reported as `File "./Logic.v", line XXX, characters XXX:` but should be `File "theories/Init/Logic.v",...

SkySkimmer

#### Description of the problem In the example below, the TC trace shows that `rewrite_strat` goes off on an entirely unnecessary goose chase when rewriting with an `eq` lemma. I...

Janno

Ltac2 precedence of field access is not consistent with Gallina

2

#### Description of the problem In Gallina, `foo bar.(baz)` means `foo (bar.(baz))`. In Ltac2, it seems to mean `(foo bar).(baz)`. #### Coq Version 8.15

JasonGross

Differences between constr, uconstr and open_constr in Tactic Notation

5

In the documentation for `Tactic Notation` (https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#tactic-notations), I'd like to add `open_constr` and briefly distinguish the following constructs. Are these descriptions correct? If not, what is correct? - `constr` means...

jfehrle

Automatic bidirectionality hints

4

Continuing from https://github.com/coq/coq/pull/13107, now with more rigid bidirectionality.

SkySkimmer

Scopes for abbreviation notations

2

Currently, notations like `Notation "'len' l" := (Z.of_nat (List.length l)) (at level 10): my_scope` can be in a scope, but abbreviations like `Notation len l := (Z.of_nat (List.length l))` (ie...

samuelgruetter