diff options
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 66d5a4f7f5..95f3955309 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -117,7 +117,7 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = in let kind = Decls.IsDefinition kind in let _ : Names.GlobRef.t = - DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs + Declare.declare_definition ~name ~scope ~kind ?hook ~impargs ~opaque:false ~poly evd ~udecl ~types ~body in () @@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c let (body, types), evd, udecl, impargs = interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in - let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in + let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in let _ : DeclareObl.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls |