Gordon Stewart

I haven't been programming Haskell recently. Is criterion now bundled with GHC? It seems this library still depends on it (https://github.com/gstew5/snarkl/blob/d6ce72b13e370d2965bb226f28a1135269e7c198/src/testsuite/benchmarks/Main.hs).

Here's the rendered version of the proposal: https://github.com/coq/ceps/blob/31bcb7d97621390f37929a908a8032ce153667ac/text/000-incremental-include.md

``` Prove x = Lemma x : type of INTERFACE.x Use x = Include (Module Tmp. Definition x := body of INTERFACE.x End Tmp). ... ``` That captures to some...

> The first UseAll should not pull in all the yn because of the dependency on Q which is not available yet, if I got it right. Yes, that's right....

@gares I do have a (pretty sketchy) implementation of some of these features in coq-elpi (that prototype prompted this CEP, in fact). I'd characterize it as a very early prototype...

> external pred coq.env.module-type i:modtypath, o:list id. This API is useful, but it didn't seem like there's currently a way to access the definitions of the terms given by `list...