Gaëtan Gilbert
Gaëtan Gilbert
Is there something stopping you from witing a PR? You already investigated the relevant code so you're possibly the most up to date on it.
>Incidentally, Pierre Boutillier is working on this issue, so, eventually, a more usable "Lemma ... with ..." will be available in a midterm future. @herbelin @pirbo so did that work...
26a5b65dfd66cbe8be1ebcf6425d6f89728690bf is the first bad commit (8.15)
I just `dune build coq-core.install` and use `_build/install/default/bin/coq_makefile`
Also you need to set COQBIN or PATH to get the right coqc
He means the same thing I said: don't iter_all_segments and instead put the name -> loc association in a summary ref. Then you don't need the code that you commented...
>I agree that iter_all_segments is bad, however I'm still not convinced that duplicating the information that is already in the libobject database scales, and moreover, it is very brittle. Scales...
>I agree on that. So either I introduce the ref in the summary as we have been doing (with all the downsides above), but the two other options I see...
>refine interface for logical objects, and extend liboject interface so kernel registration is taken care of at declaration time. That could open very interesting possibilities, but its a lot of...
>So for example, that'd open up the door to some experiments such as the one @SkySkimmer was proposing (use the kernel env for search) We don't need anything new to...