From bb46ed335e728edb5cd5fa344071dd961c031354 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 20 May 2020 00:05:50 +0200
Subject: [declare] [nit] Use proper type alias for in ProgramDecl interface

---
 vernac/declare.mli | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/vernac/declare.mli b/vernac/declare.mli
index 1172adb349..275a70fd7b 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -439,13 +439,7 @@ module ProgramDecl : sig
     -> Names.Id.t list
     -> fixpoint_kind option
     -> Vernacexpr.decl_notation list
-    -> ( Names.Id.t
-       * Constr.types
-       * Evar_kinds.t Loc.located
-       * (bool * Evar_kinds.obligation_definition_status)
-       * Int.Set.t
-       * unit Proofview.tactic option )
-       array
+    -> RetrieveObl.obligation_info
     -> (Constr.constr -> Constr.constr)
     -> t
 
-- 
cgit v1.2.3