diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/entries.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index adb3f6bd29..45b11e97ba 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -107,8 +107,3 @@ type module_entry = | MType of module_params_entry * module_struct_entry | MExpr of module_params_entry * module_struct_entry * module_struct_entry option - -(** Not used by the kernel. *) -type side_effect_role = - | Subproof - | Schema of inductive * string |