diff options
| author | Emilio Jesus Gallego Arias | 2020-06-23 23:07:04 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-26 14:38:13 +0200 |
| commit | 4ad9fa2b257184f9955216fc8345508c217c762d (patch) | |
| tree | 30d0b141653fbd6340535246420febbb44dc7f39 /vernac/classes.ml | |
| parent | d9dca86f798ce11861f1a4715763cad1aae28e5a (diff) | |
[declare] Some more cleanup on unused functions after the last commits.
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 f02474a405..ba08aa2b94 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -349,7 +349,7 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term Decls.IsDefinition Decls.Instance in let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ~hook () in - let _ : Declare.progress = + let _ : Declare.Obls.progress = Declare.Obls.add_definition ~cinfo ~info ~term ~uctx obls in () |