diff options
| author | Gaëtan Gilbert | 2019-06-13 15:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-01 13:06:22 +0200 |
| commit | 2ded4c25e532c5dfca0483c211653768ebed01a7 (patch) | |
| tree | a04b2f787490c8971590e6bdf7dd1ec4220e0290 /vernac/vernacentries.ml | |
| parent | b017e302f69f20fc4fc3d4088a305194f6c387fa (diff) | |
UIP in SProp
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f5ef5ee86f..75dfc7c3ee 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 = |