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/classes.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/classes.ml')
| -rw-r--r-- | vernac/classes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index 04321ed844..f02474a405 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -350,7 +350,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ~hook () in let _ : Declare.progress = - Obligations.add_definition ~cinfo ~info ~term ~uctx obls + Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls in () let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl ids term termtype = |