diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index e28c8e826..d50abf071 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -525,7 +525,7 @@ type side_effect_role = | Schema of inductive * string type exported_side_effect = - constant * constant_body * side_effect_role + Constant.t * constant_body * side_effect_role let export_side_effects mb env ce = match ce with |