aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/proofview.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2016-10-21 18:25:58 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2016-10-21 18:25:58 +0200
commit78eb89f254d699f1024573c39ad8ed5808245210 (patch)
treea5d67cd67f120a8168518ff57e1dc9326fec1fe7 /engine/proofview.ml
parent517cc63a18d95c02c2d2490adb110ff712d30375 (diff)
Oops, my bad, didn't expect a merge issue!
Diffstat (limited to 'engine/proofview.ml')
-rw-r--r--engine/proofview.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 208837f6a..855235d2b 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -941,7 +941,7 @@ module Unsafe = struct
let mark_as_goal evd content =
mark_in_evm ~goal:true evd content
- let advance = advance
+ let advance = Evarutil.advance
let mark_as_unresolvable p gl =
{ p with solution = mark_in_evm ~goal:false p.solution gl }