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.
---
 plugins/ltac/g_obligations.mlg | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 498b33d1a8..81ee6ed5bb 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -28,7 +28,7 @@ let () =
   let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
     snd (get_default_tactic ())
   end in
-  Obligations.default_tactic := tac
+  Declare.Obls.default_tactic := tac
 
 let with_tac f tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
@@ -78,10 +78,10 @@ GRAMMAR EXTEND Gram
 
 {
 
-open Obligations
+open Declare.Obls
 
-let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
-let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
+let obligation obl tac = with_tac (fun t -> obligation obl t) tac
+let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
 
-- 
cgit v1.2.3