diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 14 | ||||
| -rw-r--r-- | kernel/uGraph.ml | 6 |
2 files changed, 14 insertions, 6 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8b85072d6d..da77a2882e 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -936,12 +936,14 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e | DefinitionEff ce -> Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce) in - let senv, dcb = match cb.const_body with - | Def _ as const_body -> senv, { cb with const_body } - | OpaqueDef c -> - let local = empty_private cb.const_universes in - let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in - senv, { cb with const_body = OpaqueDef o } + let dcb = match cb.const_body with + | Def _ as const_body -> { cb with const_body } + | OpaqueDef _ -> + (* We drop the body, to save the definition of an opaque and thus its + hashconsing. It does not matter since this only happens inside a proof, + and depending of the opaque status of the latter, this proof term will be + either inlined or reexported. *) + { cb with const_body = Undef None } | Undef _ | Primitive _ -> assert false in let senv = add_constant_aux senv (kn, dcb) in diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 927db9e9e6..52e93a9e22 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -142,6 +142,12 @@ let enforce_leq_alg u v g = | Inl x -> x | Inr e -> raise e +let enforce_leq_alg u v g = + match Universe.is_sprop u, Universe.is_sprop v with + | true, true -> Constraint.empty, g + | true, false | false, true -> raise (UniverseInconsistency (Le, u, v, None)) + | false, false -> enforce_leq_alg u v g + (* sanity check wrapper *) let enforce_leq_alg u v g = let _,g as cg = enforce_leq_alg u v g in |