From 0683ccc035853c776d522c2bd716b18b9f39bd2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 May 2019 15:34:07 +0200
Subject: Same universe constraint fix for the checker.

---
 checker/mod_checking.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1cf07e7cc7..1b8bebb85c 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -30,13 +30,13 @@ let check_constant_declaration env kn cb =
       let env = push_context ~strict:false ctx env in
       true, env
   in
+  let ty = cb.const_type in
+  let _ = infer_type env' ty 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
   let otab = Environ.opaque_tables env in
   let body = match cb.const_body with
   | Undef _ | Primitive _ -> None
-- 
cgit v1.2.3