diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/declare.ml b/library/declare.ml index 1084aa07d..dd1b12a24 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -163,7 +163,7 @@ let hcons_constant_declaration = function let declare_constant_common id dhyps (cd,kind) = let (sp,kn) = add_leaf id (inConstant (cd,dhyps,kind)) in - let c = constant_of_kn kn in + let c = Global.constant_of_delta (constant_of_kn kn) in declare_constant_implicits c; Heads.declare_head (EvalConstRef c); Notation.declare_ref_arguments_scope (ConstRef c); |