From 170da77ad45cb0e504f82d075836a8f2965efe28 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 20 Dec 2018 15:58:24 +0100
Subject: Documentation for SProp

---
 vernac/vernacentries.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b9d0a27b39..4250ddb02c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1421,6 +1421,14 @@ let vernac_generalizable ~local =
   let local = Option.default true local in
   Implicit_quantifiers.declare_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;
-- 
cgit v1.2.3