Laurent Théry

Goals with large context

21

I have goals with very large context. When hovering over tactics. I mostly see the initial assumptions. Is there a way to activate some scrolling or at least have the...

Gauss summation rendering

8

In the paper `Untangling Mechanized Proofs` there is some nice math rendering for the proof of Gauss. How is it possible to build this locally? I've found the file `hyps.rst`...

generalize take_take and add take_takel and take_taker

3

##### Motivation for this change More generic theorem `take_take` ##### Things done/to do - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` (do not edit former entries) ##### Automatic note to reviewers...

Type inference for subtype

1

while porting some files from a tutorial by assia ([here](https://github.com/math-comp/tutorial_material/blob/716fce567244ad92adb4643f63a3d37dcb4068fb/AnIntroductionToSmallScaleReflectionInCoq/section6.v#L458)) It seems that before we could write Definition two'' : 'I_3 := Sub 2 (refl_equal true). but now we have...

Error when factorising code on subgoals

3

On 8.5 ssreflect 1.5 this works: From mathcomp Require Import all_ssreflect. Goal forall n : nat, [|| n == 1, n == 2 | n ==3] -> n < 4....

`Set Printing Xyz` options are not honored

29

I don't know if it is the intended behaviour. But when executing `Set Printing All` the command is valid only on the current goal. ``` Goal 1 = 1 ->...

Feature request : Timing

2

Just discovered the `make TIMING=1` of coq. Would be nice if `vscoq` could display in some way the info in the `.timing` files

Feedback to empty Search

3

As `Search` goes to the output window it would be nice that there will be delimitators (specially when the result is void) ```Search nat bool.``` could output ``` "Search nat...

Show number of goals

1

Would be nice to have a direct visible access to the number of open goals in the proofview. For the moment we can see (1/...) in the conclusion but this...

Error messages inside Proof View

7

Some error messages wrongly go to the proof view ``` Goal True. apply refl_equal. ```