Jan-Oliver Kaiser

Radio input fields are display: none

1

When voting on a poll, the radio input field elements are hidden. Since they carry the semantics of the voting mechanism, there is no way of voting without some kind...

shoop fails without error message

4

I have two basically identically-setup laptops here and for some reason ssh keeps failing after a few gigabytes of data. I want to try shoop and installed it on both...

Typeclass search distinguishes folded from unfolded primitive projections

9

#### Description of the problem The folded and unfolded state of `Hint Opaque` projections are not unified by `autoapply`. ```coq From Coq Require Import ssreflect. #[local] Set Primitive Projections. Class...

A brief report on trying to port the Iris hierarchy to HB

5

Hey everyone, I was very happy to see the hierarchy builder being announced and I wanted to see what would happen if I used it to define the hierarchy in...

#### 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...

MetaCoq is missing `Hint Opaque`

2

MetaCoq adds many typeclass instances for commonly used classes such as `Equivalence`, `Reflexive`, `PreOrder`, etc. Unfortunately almost all of them are on hint transparent terms which means there is a...

Enable `modulo_eta` for typeclass instance application

4

Fixes / closes #???? - [ ] Added / updated **test-suite**. - [ ] Added **changelog**. - [ ] Added / updated **documentation**. - [ ] Documented any new /...

Refine approximation of matches and unapplied functions in the bnet

44

We've had this setup at BedRock for two years or so in our own use of Coq's dnets and I don't think it ever lead to any issues whatsoever. In...

`rwHyps` changed in https://github.com/coq-community/coq-ext-lib/pull/119 and now stops on the first recursive equality it finds instead of rewriting the remaining (non-recursive) ones.

...user-specified Schema error messages