Samuel Gruetter

Response pane should not prettify text parts of error messages, but only Gallina parts

3

I got the following error message display in the response pane: ``` Error: containsProgram already ∃. ``` but I would prefer it to be: ``` Error: containsProgram already exists. ```...

PG highlights beginning of conclusion like a hypothesis name

4

```coq Notation "a -:" := (id a) (at level 9, format "a -:"). Lemma test(foo: nat) : foo-: = foo. ``` displays ``` foo : nat ============================ foo-: = foo...

PG goes bananas (accepts any string after `{|`)

2

The following file is accepted by PG: ```coq Goal False. Proof. {| Hello this is cool. {| Is this a new kind of comment? . {| Multi-line works as well!....

PG accepts `}.` but `coqc` doesn't

1

I can step through the following file in proof general without getting any errors: ```coq Goal True /\ True. Proof. split. { exact I. }. { exact I. }. Qed....

Ltac2 messages are not displayed in *response* buffer if there's timing output

3

Not sure if this is a PG issue or an Ltac2 issue, but here's something that works fine in Ltac1 but not in Ltac2: ```coq Ltac wait1 n := idtac...

Goals window not refreshing after `Proof.`

2

If I open this file, ```coq Goal False. Proof. ``` jump to the last line, and hit `C-c C-Enter`, the goals window remains empty. Desired behavior: It should show ```...

Invoke QuickChick on current goal

11

Hi QuickChick developers, congrats on the recent developments, I think QuickChick has become much cooler since I looked at it the last time :tada: (or maybe it's just that the...

QuickChick version: 1.0.2 Coq version: 8.8.1 I realize this one might be tricky, but raising the issue anyways in case someone has a good idea: I'd like to use the...

command line quickChick tool prints counterexample too early

1

QuickChick version: 1.0.2 Coq version: 8.8.1 A small but annoying bug about the `quickChick` command line tool: It displays the counterexample before displaying the title `Checking LEMMA_NAME...`. Should be reproducible...

Examples from bedrock2 compiler where QuickChick cannot automatically derive Checkable

1

If you run ``` grep -R . --include='*.v' -e 'TC_FAIL' -C7 ``` inside the directory https://github.com/samuelgruetter/counterexamples/tree/bda5b7dbd74ee873ca360b67c699482918f9d4e0/coq, you will find a few QuickChick queries marked with `TC_FAIL` where QuickChick fails to...