diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/term_typing.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index c44adad5cb..da0326981c 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -202,7 +202,10 @@ let infer_declaration env kn dcl = let j = infer env body in let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in - let def = Def (Mod_subst.from_val def) in + let def = + if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) + else Def (Mod_subst.from_val def) + in def, typ, None in feedback_completion_typecheck feedback_id; |