Sampsa Kiiskinen

Assertion failed in pretty printing

1

See coq/coq#9360. #### Notes I reported this bug to the Coq project with a reference in the QuickChick project, because I do not know whether this bug is caused by...

#### Version Coq 8.15.0 Equations 1.3 #### Operating system Red Hat Enterprise Linux Workstation 7.4 #### Description of the problem The following program hangs on `funelim`. ```coq From Coq Require...

Simplification gets stuck or diverges in simple use cases

9

#### Version Coq 8.13.2 Equations 1.2.4 #### Operating system Red Hat Enterprise Linux Workstation 7.4 #### Description of the problem The following definition via equations cannot be simplified by any...

Anonymous implicit generalization is not recognized

3

## Versions Coq 8.15.0 Coqtail 1.6.2 Vim 8.2 Equations 1.3 Python 3.7.4 ## Description Unnamed parameters introduced by implicit generalization are highlighted as if they were named parameters without explicit...

Search results incorrectly highlighted as errors

3

## Versions Coq 8.15.0 Coqtail 1.6.2 Vim 8.2 Equations 1.3 Python 3.7.4 ## Description Search results for lemmas, whose names end in `error`, are highlighted as if they were errors...

Row and column backgrounds are woven in a strange way

1

## Versions Coq 8.15.0 Coqtail 1.6.2 Vim 8.2 Equations 1.3 Python 3.7.4 ## Description This is not so much of a bug as it is a peculiar interaction of features,...

Different bullets have different formatting behavior

3

## Versions Coq 8.15.0 Coqtail 1.6.2 Vim 8.2 Equations 1.3 Python 3.7.4 ## Description If you try to open a new line after a line that starts with a bullet,...

Inconsistent options in auxiliary buffers

2

## Versions Coq 8.15.0 Coqtail 1.6.2 Vim 8.2 Equations 1.3 Python 3.7.4 ## Description There are various options that are intended to be used in the script view, but also...

Capturing streams on Windows uses the standard streams instead of dedicated pipes. There are only two standard streams, so assertions are mixed with other output. Using a named pipe should...

The applicative instance for lists does not behave the way it should. Compare the following Racket program with the Haskell program following it to observe the crucial difference. ``` scm...