diff options
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 = |