aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cbytecodes.mli')
-rw-r--r--kernel/cbytecodes.mli1
1 files changed, 0 insertions, 1 deletions
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 03b6bc619..238edc0af 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -30,7 +30,6 @@ val last_variant_tag : tag
type structured_constant =
| Const_sort of Sorts.t
| Const_ind of inductive
- | Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
| Const_univ_level of Univ.Level.t