aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/obligations.ml')
-rw-r--r--vernac/obligations.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1f401b4e1..14d764232 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -220,7 +220,7 @@ let eterm_obligations env name evm fs ?status t ty =
in
let loc, k = evar_source id evm in
let status = match k with
- | Evar_kinds.QuestionMark (o,_) -> o
+ | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o
| _ -> match status with
| Some o -> o
| None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))