Yves Bertot

Checking that all new lemmas, Exports modules, and Canonical Structures are exported in ssralg.v

12

This is a continuation of #425. The wish is to automate the verification that all new lemmas, canonical structures, and Export modules are duly exported by the GRing.Theory module, module...

Wrong error message when trying to unfold with a pattern

6

``` From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Unset Strict Implicit. Set Printing Implicit Defensive. Lemma toto : 3 + 12 = 5 + 12. Proof. rewrite [3 +...

Failure of automatic lemma invocation

4

Adding a lemma and placing a hint on this lemma, I am able to construct to goals that are apparently the same, but one is solved automatically while the other...

[WIP]removed deprecation warnings and most duplicate clear warnings

6

Current version has two duplicate-clear warnings that require a little more thinking.

Preparation of a release version for coq-8.16

8

Not really an issue, just a report about work in progress. A branch coq-v8.16 is currently available at https://github.com/ybertot/coq-dpdgraph/commit/4728cb8e752594ac1c2f186dee6b2dd8e2cfead7 This branch should be all ready for creating the necessary files...

avoid warnings emitted by Coq

8

Only modifications in the Coq source files.

an attempts at reducing false alarms by sorting oracle files and logs

1

If this is merged, tests will be slightly less precise but will be resistant to some changes in order of lines. We may consider that the occasions where sorting is...

After the merge of PR#74 make tests reports changes that are not relevant. Files are mostly the same, except the order of lines has changed. We should compare logs with...