From ef72be87579be34e9454fe1f785ff36a9c25246c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 3 Aug 2014 21:16:44 +0200
Subject: - Fix handling of opaque polymorphic definitions which were turned
 transparent. - Decomment code in reductionops forgotten after debugging.

---
 kernel/term_typing.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index c44adad5cb..da0326981c 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -202,7 +202,10 @@ let infer_declaration env kn dcl =
 	  let j = infer env body in
 	  let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
 	  let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
-	  let def = Def (Mod_subst.from_val def) in
+	  let def = 
+	    if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
+	    else Def (Mod_subst.from_val def) 
+	  in
 	    def, typ, None
       in
 	feedback_completion_typecheck feedback_id;
-- 
cgit v1.2.3