From b247761476c4b36f0945c19c23c171ea57701178 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 6 Oct 2016 18:02:25 +0200
Subject: Fix for bug #4863, update the Proofview's env with

side_effects. Partial solution to the handling of side effects
in proofview.
---
 kernel/entries.mli | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'kernel/entries.mli')

diff --git a/kernel/entries.mli b/kernel/entries.mli
index f94068f31e..8e8e97d615 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -97,7 +97,12 @@ type module_entry =
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
 
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type seff_env =
+  [ `Nothing
+  (* The proof term and its universes.
+     Same as the constant_body's but not in an ephemeron *)
+  | `Opaque of Constr.t * Univ.universe_context_set ]
 
 type side_eff =
   | SEsubproof of constant * Declarations.constant_body * seff_env
-- 
cgit v1.2.3