From 4a2c8653c0b2f5e73db769a8ea6bf79b76086524 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 23 Jun 2020 22:36:22 +0200
Subject: [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.
---
 vernac/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/classes.ml')

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 =
-- 
cgit v1.2.3