Same universe constraint fix for the checker.

1 files 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