Documentation for SProp

1 files changed, 8 insertions, 0 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b9d0a27b39..4250ddb02c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1424,6 +1424,14 @@ let vernac_generalizable ~local =
 let () =
   declare_bool_option
     { optdepr  = false;
+      optname  = "allow sprop";
+      optkey   = ["Allow";"StrictProp"];
+      optread  = (fun () -> Global.sprop_allowed());
+      optwrite = Global.set_allow_sprop }
+
+let () =
+  declare_bool_option
+    { optdepr  = false;
       optname  = "silent";
       optkey   = ["Silent"];
       optread  = (fun () -> !Flags.quiet);