From 5eda6e5c0f4875c0222eeba5d1210b7ec59f5496 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 26 May 2019 02:34:14 +0200
Subject: Ensure dynamically that non-opaque definitions are always side-effect
 free.

It is guaranteed by Declare, but a little dynamic check does not hurt.
---
 kernel/term_typing.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel')

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
-- 
cgit v1.2.3