diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 44 |
1 files changed, 23 insertions, 21 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index faa4411e92..9e33b431fc 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -154,7 +154,7 @@ the polymorphic case let c = Constr.hcons j.uj_val in feedback_completion_typecheck feedback_id; c, uctx) in - let def = OpaqueDef (Opaqueproof.create proofterm) in + let def = OpaqueDef proofterm in { Cooking.cook_body = def; cook_type = tyj.utj_val; @@ -207,7 +207,7 @@ the polymorphic case in let def = Constr.hcons (Vars.subst_univs_level_constr usubst j.uj_val) in let def = - if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) + if opaque then OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) else Def (Mod_subst.from_val def) in feedback_completion_typecheck feedback_id; @@ -232,7 +232,7 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let build_constant_declaration _kn env result = +let build_constant_declaration ~force ~iter env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -271,11 +271,8 @@ let build_constant_declaration _kn env result = | Undef _ | Primitive _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> - let vars = - global_vars_set env - (Opaqueproof.force_proof (opaque_tables env) lc) in - (* we force so that cst are added to the env immediately after *) - ignore(Opaqueproof.force_constraints (opaque_tables env) lc); + let (lc, _) = force lc in + let vars = global_vars_set env lc in if !Flags.record_aux_file then record_aux env ids_typ vars; vars in @@ -296,11 +293,14 @@ let build_constant_declaration _kn env result = check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) - OpaqueDef (Opaqueproof.iter_direct_opaque (fun c -> - let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env c in - let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in - check declared inferred) lc) in + let kont c = + let ids_typ = global_vars_set env typ in + let ids_def = global_vars_set env c in + let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in + check declared inferred + in + OpaqueDef (iter kont lc) + in let univs = result.cook_universes in let tps = let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in @@ -318,8 +318,10 @@ let build_constant_declaration _kn env result = (*s Global and local constant declaration. *) -let translate_constant mb env kn ce = - build_constant_declaration kn env +let translate_constant mb env _kn ce = + let force cu = Future.force cu in + let iter k cu = Future.chain cu (fun (c, _ as p) -> k c; p) in + build_constant_declaration ~force ~iter env (infer_declaration ~trust:mb env ce) let translate_local_assum env t = @@ -327,8 +329,10 @@ let translate_local_assum env t = let t = Typeops.assumption_of_judgment env j in j.uj_val, t -let translate_recipe ~hcons env kn r = - build_constant_declaration kn env (Cooking.cook_constant ~hcons r) +let translate_recipe ~hcons env _kn r = + let force o = Opaqueproof.force_direct o in + let iter k o = Opaqueproof.iter_direct_opaque k o in + build_constant_declaration ~force ~iter env (Cooking.cook_constant ~hcons r) let translate_local_def env _id centry = let open Cooking in @@ -351,8 +355,7 @@ let translate_local_def env _id centry = | Def _ -> () | OpaqueDef lc -> let ids_typ = global_vars_set env typ in - let ids_def = global_vars_set env - (Opaqueproof.force_proof (opaque_tables env) lc) in + let ids_def = global_vars_set env (fst (Future.force lc)) in record_aux env ids_typ ids_def end; let () = match decl.cook_universes with @@ -362,8 +365,7 @@ let translate_local_def env _id centry = let c = match decl.cook_body with | Def c -> Mod_subst.force_constr c | OpaqueDef o -> - let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in - let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in + let (p, cst) = Future.force o in (** Let definitions are ensured to have no extra constraints coming from the body by virtue of the typing of [Entries.section_def_entry]. *) let () = assert (Univ.ContextSet.is_empty cst) in |