Merge PR #10252: Various dynamic assertions and cleanups in opaque typing

Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
Ack-by: ppedrot

1 files changed, 2 insertions, 2 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1bc5891517..dedbddfee0 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -29,13 +29,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