aboutsummaryrefslogtreecommitdiff
path: root/checker/checkFlags.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-06-13 15:39:43 +0200
committerGaëtan Gilbert2020-07-01 13:06:22 +0200
commit2ded4c25e532c5dfca0483c211653768ebed01a7 (patch)
treea04b2f787490c8971590e6bdf7dd1ec4220e0290 /checker/checkFlags.ml
parentb017e302f69f20fc4fc3d4088a305194f6c387fa (diff)
UIP in SProp
Diffstat (limited to 'checker/checkFlags.ml')
-rw-r--r--checker/checkFlags.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml
index 1f5e76bd83..369623e8c5 100644
--- a/checker/checkFlags.ml
+++ b/checker/checkFlags.ml
@@ -18,6 +18,7 @@ let set_local_flags flags env =
check_universes = flags.check_universes;
conv_oracle = flags.conv_oracle;
cumulative_sprop = flags.cumulative_sprop;
+ allow_uip = flags.allow_uip;
}
in
Environ.set_typing_flags flags env