diff options
| author | Emilio Jesus Gallego Arias | 2020-06-23 22:36:22 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:13 +0200 |
| commit | 4a2c8653c0b2f5e73db769a8ea6bf79b76086524 (patch) | |
| tree | 0c1013329f008ef645c7b7712ccf55be72d39c25 /vernac/comDefinition.ml | |
| parent | 06159c53e84ab1cff0299890767576972eaf83c2 (diff) | |
[declare] Merge remaining obligations bits into Declare
This allows us to remove a large chunk of the internal API, and is the
pre-requisite to get rid of [Proof_ending], and even more refactoring
on the declare path.
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 537f713e82..5860626917 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -127,10 +127,9 @@ 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, typ, uctx, obls = Declare.prepare_obligation ~name ~body ~types evd in + let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in let _ : Declare.progress = let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in - Obligations.add_definition - ~cinfo ~info ~term ~uctx obls + Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls in () |