aboutsummaryrefslogtreecommitdiff
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/values.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/values.ml b/checker/values.ml
index 907f9f7e32..f7a367b986 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -240,7 +240,7 @@ let v_template_universes =
v_tuple "template_universes" [|List(Opt v_level);v_context_set|]
let v_primitive =
- v_enum "primitive" 50 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
+ v_enum "primitive" 54 (* Number of constructors of the CPrimitives.t type *)
let v_cst_def =
v_sum "constant_def" 0