diff options
| -rw-r--r-- | kernel/term_typing.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index af2c511db9..eea04bbf9a 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -174,6 +174,7 @@ the polymorphic case let body, ctx = match trust with | Pure -> body, ctx | SideEffects handle -> + let () = assert opaque in let body, ctx', _ = handle env body side_eff in body, Univ.ContextSet.union ctx ctx' in |