diff options
Diffstat (limited to 'kernel/cPrimitives.mli')
| -rw-r--r-- | kernel/cPrimitives.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index f9424fb09d..3e6ec8dbcc 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -74,7 +74,7 @@ type 'a prim_ind = | PIT_carry : prim_type prim_ind | PIT_pair : (prim_type * prim_type) prim_ind | PIT_cmp : unit prim_ind - | PIT_option : unit prim_ind + | PIT_f_cmp : unit prim_ind type prim_ind_ex = PIE : 'a prim_ind -> prim_ind_ex |