Meven Lennon-Bertrand

I got a similar issue (in version 1.3+8.14) with an example boiling down to: ```coq From Equations Require Import Equations. Equations test (n : nat) : nat := test 1...

Using `dmesg` I get ``` [ 4920.969314] oom-kill:constraint=CONSTRAINT_NONE,nodemask=(null),cpuset=/,mems_allowed=0,global_oom,task_memcg=/user.slice/user-1000.slice/[email protected],task=coqidetop.opt,pid=10508,uid=1000 [ 4920.969334] Out of memory: Killed process 10508 (coqidetop.opt) total-vm:2993924kB, anon-rss:2111052kB, file-rss:0kB, shmem-rss:0kB, UID:1000 pgtables:4432kB oom_score_adj:0 ``` so indeed it is looks...

Nothing heavy, no – probably a browser with a few open tabs, maybe another Electron-based application.

Just wanting to report that I encountered a similar issue. I have had a working opam-based setup for a while, but wanted to switch to the platform instead, and ran...

Here it is: ``` \documentclass{article} \usepackage{sidenotes} \begin{document} This is a text% \sidenote{This is a side-note.} with a footnote in the middle. \end{document} ``` which gives two warnings: ``` 'textThis': Possible...

I agree, I like the semi-colon too! Your solution seems better than mine, I think in this case it might be a lack of documentation about the option `noenddot` option...

I can confirm that, I definitely encounter figures that run off the page instead of being moved around. I can indeed counter this by moving the figure higher, exchanging them,...

Sorry to ping you @mattam82, but I'm still somewhat blocked because of this, any chance of getting HoTT back on track soon-ish?

Alternative approach: make the difference also in PCUIC, and redefine the current field accessors to functions which do the merging (or keep them as fields + proofs that they correspond...

> The algorithm is written in highly dependent style to show termination, and does not compute inside Rocq itself. I think an extensionally equivalent fuel-based variant can be written easily...