aboutsummaryrefslogtreecommitdiff
path: root/checker/values.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-04-14 16:19:19 +0000
committerGitHub2021-04-14 16:19:19 +0000
commit00391bd681098132cc89c356d1d27334d257fc8b (patch)
tree9bb7bc653fd98b120ab5f80e2475141f85ad841f /checker/values.ml
parent90a6c01dec9d58fa409e7097ac5ba03f08a9ae7b (diff)
parent8df5a37d934b4f862a6183ee451c6bb34ae72d94 (diff)
Merge PR #14050: Remove remote counter system
Reviewed-by: gares Ack-by: ppedrot Ack-by: ejgallego
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 f7a367b986..1353435181 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -87,7 +87,7 @@ let v_cons = v_tuple "constructor" [|v_ind;Int|]
(** kernel/univ *)
-let v_level_global = v_tuple "Level.Global.t" [|v_dp;Int|]
+let v_level_global = v_tuple "Level.Global.t" [|v_dp;String;Int|]
let v_raw_level = v_sum "raw_level" 3 (* SProp, Prop, Set *)
[|(*Level*)[|v_level_global|]; (*Var*)[|Int|]|]
let v_level = v_tuple "level" [|Int;v_raw_level|]