From db391451c5f89c034e6fec1b10fec66a25e3d4d4 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 4 Nov 2019 19:14:07 -0800
Subject: Replace "option" in doc when it refers to a flag

---
 stm/stm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index c399b69a77..2b68e1778d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2892,7 +2892,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ())
       | VtStartProof (guarantee, names) ->
 
          if not (get_allow_nested_proofs ()) && VCS.proof_nesting () > 0 then
-           "Nested proofs are not allowed unless you turn option Nested Proofs Allowed on."
+           "Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on."
            |> Pp.str
            |> (fun s -> (UserError (None, s), Exninfo.null))
            |> State.exn_on ~valid:Stateid.dummy newtip
-- 
cgit v1.2.3