aboutsummaryrefslogtreecommitdiff
path: root/engine/proofview.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-09-01 11:51:41 +0200
committerPierre-Marie Pédrot2020-09-01 11:51:41 +0200
commit0d30f79268fea18ef99c040a859956f61c3d978a (patch)
tree26694ab196e67dde80cc8489236770bda59a061c /engine/proofview.ml
parent46768229c5349aa92a8107cd0a6ded32fd22d768 (diff)
parent576c1153dae2b3660d35127862aeb3d528eb6d8d (diff)
Merge PR #12892: Update update_global_env usage
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r--engine/proofview.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 2fc5ade0d2..5b0e6f5785 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1037,8 +1037,8 @@ module Unsafe = struct
let mark_as_unresolvables p evs =
{ p with solution = mark_in_evm ~goal:false p.solution evs }
- let update_sigma_env pv env =
- { pv with solution = Evd.update_sigma_env pv.solution env }
+ let update_sigma_univs ugraph pv =
+ { pv with solution = Evd.update_sigma_univs ugraph pv.solution }
end