aboutsummaryrefslogtreecommitdiff
path: root/checker/values.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/values.ml')
-rw-r--r--checker/values.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 0de8a3e03f..628089433a 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -217,7 +217,7 @@ let v_cst_def =
[|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
let v_typing_flags =
- v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool|]
+ v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]