Jason Gross

Sorry, apparently shift+enter or ctrl+enter closes a bug. I think that `transparent_abstract` is also an important tactic, and it's very important to be able to use this in non-top-level position....

@SkySkimmer Your suggestions breaks a lot of use cases, such as `abstract exact_no_check ...` and `abstract vm_no_check ...`. Also the use of `abstract` to compactify the evarmarp(?), which is quite...

@SkySkimmer The point of `abstract exact_no_check` is "this conversion problem is so expensive that I want to guarantee it only goes through the kernel once; at the same time, I...

@SkySkimmer re "don't know what compactify means." I believe this is the behavior of the `Optimize Proof` vernacular. For reasons I don't fully understand, replacing `omega` with `abstract omega` can...

I think the current state of things is that we can support a full-featured `transparent_abstract` with @SkySkimmer 's proposal (at the cost of it sharing less code with `abstract`?). If...

@SkySkimmer I don't have a super-good example, but here's an example not using `abstract` increases memory usage by about 25% (from about 2.5 GB to about 3.2 GB): https://github.com/mit-plv/fiat-crypto/blob/de373c3df74344cf5fe1ba2b2f21087f1be7d8e9/src/Curves/Weierstrass/AffineProofs.v#L48 With...

> Your point about abstract is an interesting one; cc #9146 ; I am not sure the view where abstract does modify document state is the one we want; I'd...

> I wasn't sure where to put tests for this and how they should look but I tested it outside the automatic test-suite with the following coq code: I think...

Also, congratulations on making your first PR!

> 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. Isn't...