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/comDefinition.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'vernac/comDefinition.ml')

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