Skip to content

Commit

Permalink
Merge pull request #672 from ppedrot/fast-global-env
Browse files Browse the repository at this point in the history
Directly set universes in the global wrapper.
  • Loading branch information
gares authored Jul 19, 2024
2 parents 62f6588 + e049976 commit 7830cea
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/coq_elpi_HOAS.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
;;

Expand Down

0 comments on commit 7830cea

Please sign in to comment.