aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof.ml')
-rw-r--r--proofs/proof.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index d7904c56a8..616cbf9678 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -353,8 +353,8 @@ let compact p =
let entry, proofview = Proofview.compact p.entry p.proofview in
{ p with proofview; entry }
-let update_sigma_env p env =
- let proofview = Proofview.Unsafe.update_sigma_env p.proofview env in
+let update_sigma_univs ugraph p =
+ let proofview = Proofview.Unsafe.update_sigma_univs ugraph p.proofview in
{ p with proofview }
(*** Function manipulation proof extra informations ***)