Merge PR #10390: UIP in SProp

Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes

1 files changed, 9 insertions, 0 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 65af66435b..b0e483ee74 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1553,6 +1553,15 @@ let () =
       optread  = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
       optwrite = (fun b -> Global.set_check_universes b) }
 
+let () =
+  declare_bool_option
+    { optdepr  = false;
+      optkey   = ["Definitional"; "UIP"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.allow_uip);
+      optwrite = (fun b -> Global.set_typing_flags
+                     {(Global.typing_flags ()) with Declarations.allow_uip = b})
+    }
+
 let vernac_set_strategy ~local l =
   let local = Option.default false local in
   let glob_ref r =