Thomas Lamiaux

Add an option to control the printing panel

2

When you are writing in the code `Print x` then it prints it the definition in the proof window. However, when you are using `Coq: Print` it prints in the...

Warning for inlining Signature for

4

A warning > Automatically inlined signature for type vec. Use [Derive Signature for vec.] to avoid this. Is triggered when deriving NoConfusionHom but not when deriving NoConfusion. I would have...

Deeplim inverses some equalities when sections are involved

1

I found a weird behavior with depelim. In the code below, depelim keeps inverting the equality ``` Section Foo. Context (x y : vec nat 2). Definition foo (H :...