Jan Stolarek

Same problem on Debian 10. On Debian the SHA header file is part of `libssl-dev`, so on Debian these two lines in the source code presumably should say: ``` #include...

Minor update: this does not happen with every tactic. For example `rewrite

[Here](https://github.com/jstolarek/scripts/blob/master/emacs/.emacs#L133) are my proof general settings. My Emacs is 24.5.1

> Can you try turning company-mode off? (M-x company-mode). I'd guess this is probably the main factor. Sadly, turning it off does not help :( > as you pointed out,...

Let me know if there is any debugging info I can provide. > Support for bracketed paste is supported in most recent terminal emulator I wonder how recent - I...

> Would this work instead? Don't type Set P for Set Printing Implicit; use SPI. This would work for me - I used to program in Java, where this is...

Ha! Somehow it did not cross my mind to actually try it out :-) Need to change my muscle-memory to Java style.

Design question: do we actually require that each big lambda gives rise to a forall variable? If that would be the case then the implication is we also permit unused...

Random guess: are we crucially relying on [`repr`](https://github.com/links-lang/links/blob/master/core/unionfind.ml#L62) during type inference? This caused me a lot of headache in inferno - gory details [here](https://github.com/jstolarek/inferno/issues/34#issuecomment-769188660). I wouldn't be surprised to see...

Maybe we could also enable `recheck_frontend_transformations` in the `examples_default.config`. That requires that we fix #871 first (because now the prelude does not typecheck) and investigate performance impact.