Emilio Jesús Gallego Arias

Thanks for the feedback @JasonGross ; we will see what we can do, but unfortunately it seems that we are facing a bad dilemma to have here: the current implementation...

Umm, I'm afraid we won't be able to have our cake and eat it too... Well, let's keep thinking. I do agree about the eager typechecking stuff being useful, we...

> Maybe that's just the effect of running nf_evars on stuff, if that's the case maybe we could provide it as a tactic, I dunno. If you look at `cache_term_by_tactic_then`...

Very interesting discussion @andres-erbsen , thanks. In fact quite a few of the pitfalls you both comment are IMHO related to other problems in the proof/tactic engine; however I have...

Actually @afdw was asking me today about why we ever need to perform `nf_evar` instead of being fully under demand; ccing her so she can follow the discussion.

@bmwiedemann I'm afraid I cannot understand that graph, how come `ocamlc stream.mli` is called twice?

@bmwiedemann indeed if you called dune build twice, since a while, dune won't allow this to happen in parallel. That graph seems strange to me. Second graph looks normal (one...

@coqbot run full CI

CI seems good, except for a trivial SerAPI overlay.

> Not sure there's much value in putting some `[@ocaml.warning "-3"]` in various places. What would you do? It would be nice indeed to remove these ones, but it is...