1 files changed, 24 insertions, 8 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 1dd16f1630..9b41fbcb7a 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -8,6 +8,13 @@ open Environ
 
 (** {6 Checking constants } *)
 
+let indirect_accessor = ref {
+  Opaqueproof.access_proof = (fun _ _ -> assert false);
+  Opaqueproof.access_discharge = (fun _ _ -> assert false);
+}
+
+let set_indirect_accessor f = indirect_accessor := f
+
 let check_constant_declaration env kn cb =
   Flags.if_verbose Feedback.msg_notice (str "  checking cst:" ++ Constant.print kn);
   (* Locally set the oracle for further typechecking *)
@@ -16,23 +23,32 @@ let check_constant_declaration env kn cb =
   (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
-    | Monomorphic ctx -> false, push_context_set ~strict:true ctx env
+    | Monomorphic ctx -> false, env
     | Polymorphic auctx ->
       let ctx = Univ.AUContext.repr auctx in
       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
+  let otab = Environ.opaque_tables env' in
+  let body, env' = match cb.const_body with
+  | Undef _ | Primitive _ -> None, env'
+  | Def c -> Some (Mod_subst.force_constr c), env'
+  | OpaqueDef o ->
+    let c, u = Opaqueproof.force_proof !indirect_accessor otab o in
+    let env' = match u, cb.const_universes with
+    | Opaqueproof.PrivateMonomorphic (), Monomorphic _ -> env'
+    | Opaqueproof.PrivatePolymorphic (_, local), Polymorphic _ ->
+      push_subgraph local env'
+    | _ -> assert false
+    in
+    Some c, env'
+  in
   let () =
-    match Environ.body_of_constant_body env cb with
+    match body with
     | Some bd ->
-      let j = infer env' (fst bd) in
+      let j = infer env' bd in
       (try conv_leq env' j.uj_type ty
        with NotConvertible -> Type_errors.error_actual_type env j ty)
     | None -> ()