MackieLoeffel

This just addresses the second point (jumping to the original source instead of dune's copy in jump-to-definition). You still need to have a _CoqProject file with the right paths.

I don't know what the difference between the ATmega32 and other AVR microcontrollers is. The main functionallity of this project is the decoding and emulation of instructions. So if the...

Thanks for creating this PR! I think the definitions provided by this PR fill an important hole in the Coq standard library. I needed a library for fixed sized integers...

A simpler testcase that does not require Utf8 is the following: ``` Lemma test : Truea. ``` PG shows an error on first line for me, but it should be...

I am currently using the following in my `.emacs` file to automatically set `proof-shell-strip-crs-from-input` to `t`: ``` (add-hook 'coq-shell-mode-hook (lambda () (setq proof-shell-strip-crs-from-input t))) ``` (`custom-set-variables` does not work since...

> Side note: please don't quote your lambdas. Indeed, thanks! I edited my message above in case someone copies it to their .emacs file.

One workaround is to add a new hook after the hook from proof general and set the variables to the desired values there: ```elisp (add-hook 'proof-shell-before-process-hook (lambda () (setq proof-prog-name...

Thanks for this proposal! I think this would be very useful for the proof automation I am working on. I've often encountered the problem that I would like to use...