diff options
| author | Gaëtan Gilbert | 2020-05-19 14:12:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-19 14:12:30 +0200 |
| commit | 407ca661d7eb33afed706afe74f11fccac2f1dd4 (patch) | |
| tree | d867bc7f77bfeb1c9a09598f7945d7d77f1ccae3 /vernac/comDefinition.ml | |
| parent | 2222e455f0501b700f198ab614d8743229062f73 (diff) | |
| parent | 833d7672a4cc1dbdd4ab5a861362824b03f72d57 (diff) | |
Merge PR #12301: [declare] Grand unification of the proof save path.
Reviewed-by: SkySkimmer
Ack-by: ppedrot
Diffstat (limited to 'vernac/comDefinition.ml')
| -rw-r--r-- | vernac/comDefinition.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 95f3955309..eac8f92e2e 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -127,7 +127,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c interp_definition ~program_mode udecl bl ~poly red_option c ctypopt in let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in - let _ : DeclareObl.progress = + let _ : Declare.Obls.progress = Obligations.add_definition ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls in () |