aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/subtac_obligations.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac/subtac_obligations.ml')
-rw-r--r--contrib/subtac/subtac_obligations.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 769aff9dc..5e7f025be 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -58,7 +58,7 @@ let subst_deps obls deps t =
let xobl = obls.(x) in
debug 3 (str "Trying to get body of obligation " ++ int x);
let oblb =
- try out_some xobl.obl_body
+ try Option.get xobl.obl_body
with _ ->
debug 3 (str "Couldn't get body of obligation " ++ int x);
assert(false)