diff options
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index dc9c8e2d3c..cb9acda770 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -203,6 +203,8 @@ let context_insection sigma ~poly ctx = else Monomorphic_entry Univ.ContextSet.empty in let entry = Declare.definition_entry ~univs ~types:t b in + (* XXX Fixme: Use DeclareDef.prepare_definition *) + let entry = DeclareDef.ClosedDef.of_proof_entry entry in let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry in |