Laurent Théry
Laurent Théry
maybe giving the possibility to display only the assumptions that have changed would be nice
I was thinking more on something in the line of [this](https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#showing-differences-between-proof-steps) where one displays onl waht has changed.
I guess in my context as the context is very large, diff with sibling or ancestor both would do the trick. but I understand it could be difficult to do...
> how do you determine which old goal to compare a new goal against when computing diffs? Apparently `diffs` compares with the state before the tactical call which seems reasonable....
not sure the `diff` works well with focus.
> does it work for you? Yep :+1: ``` Then, we add notations to print LaTeX code (this is only one way to do it; another way would be to...
Tried the Notation version on an example of `mathcomp` that uses binomial, product, summation and polynomial : It looks really good I think : [digit](http://www-sop.inria.fr/marelle/lucas/digitn.html) :smile: Still I had some...
Thanks, I've managed to somewhat reduce the overboxing by adding a newline when displaying a forall. For the post-processing, too difficult for me as I don't know much the technology....
In the theorems of [fp.rst](http://www-sop.inria.fr/marelle/lucas/fp.rst) i would like variables like *p1* and *p2* to be *p1* and *p2*
could it be the definition of angle?