From e04997656299954d1760e62c2723214104f02bfb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 19 Jul 2024 12:57:51 +0200 Subject: [PATCH] Directly set universes in the global wrapper. We trust that the set of universes in the evarmap is synchronized with the global environment, which allows setting the constraints in O(1) instead of pushing them in superlinear time. This is seemingly critical for some clients of coq-elpi. --- src/coq_elpi_HOAS.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 2aa9d3c3c..da10f6ff0 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -3614,7 +3614,7 @@ let get_current_env_sigma ~depth hyps constraints state = let get_global_env_current_sigma ~depth hyps constraints state = let state, _, changed, gls = elpi_solution_to_coq_solution ~eta_contract_solution:true ~calldepth:depth constraints state in let coq_ctx = mk_coq_context ~options:(get_options ~depth hyps state) state in - let coq_ctx = { coq_ctx with env = Environ.push_context_set (Evd.universe_context_set (get_sigma state)) coq_ctx.env } in + let coq_ctx = { coq_ctx with env = Environ.set_universes (Evd.universes (get_sigma state)) coq_ctx.env } in state, coq_ctx, get_sigma state, gls ;;