From 70c4c510e5d8817aad27a5053e813d82f869e52f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 19 May 2020 23:51:11 +0200
Subject: [nit] Remove `Declare.Obls.err_not_transp`

Not necessary anymore after the merge of obligation declaration into
the main path.
---
 vernac/declare.mli | 1 -
 1 file changed, 1 deletion(-)

diff --git a/vernac/declare.mli b/vernac/declare.mli
index 62bc6a34bf..1172adb349 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -517,7 +517,6 @@ val obl_substitution :
   -> (Id.t * (Constr.types * Constr.types)) list
 
 val dependencies : Obligation.t array -> int -> Int.Set.t
-val err_not_transp : unit -> unit
 
 (* This is a hack to make it possible for Obligations to craft a Qed
  * behind the scenes.  The fix_exn the Stm attaches to the Future proof
-- 
cgit v1.2.3