Dear masters of the universe, after a Coq call I wrote this API
I'm using it in coq-elpi and I'm happy with its behavior, but the performances are ugly. Can it be implemented in a better way?
For the record, a silly coq-elpi API, like opening/closing a module, takes 0.000072s without calling demote, but 0.000746s calling it O_o (I'm calling it after every API that has an impact on the global environment)
CC @Cyril Cohen
Actually, that timing is with/without commenting this line
let sigma = Evd.from_ctx (UState.demote_global_univs env (Evd.evar_universe_context sigma)) in
So I guessed the culprit is demote.
Last updated: Dec 01 2023 at 04:01 UTC