From ed04b8eb07ca3925af852c30a75c553c134f7d72 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 29 Oct 2018 17:56:10 +0100
Subject: Local universes for opaque polymorphic constants.

---
 checker/mod_checking.ml | 8 +++++++-
 checker/values.ml       | 1 +
 2 files changed, 8 insertions(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ed617d73c2..c36d96f2ba 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -20,7 +20,13 @@ let check_constant_declaration env kn cb =
     | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env
     | Polymorphic_const auctx ->
       let ctx = Univ.AUContext.repr auctx in
-      true, push_context ~strict:false ctx env
+      let env = push_context ~strict:false ctx env in
+      true, env
+  in
+  let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with
+    | None, _ -> env'
+    | Some local, (OpaqueDef _, true) -> push_subgraph local env'
+    | Some _, _ -> assert false
   in
   let ty = cb.const_type in
   let _ = infer_type env' ty in
diff --git a/checker/values.ml b/checker/values.ml
index 0de8a3e03f..388123baaf 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -227,6 +227,7 @@ let v_cb = v_tuple "constant_body"
     v_constr;
     Any;
     v_const_univs;
+    Opt v_context_set;
     v_bool;
     v_typing_flags|]
 
-- 
cgit v1.2.3