aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--vernac/declare.mli8
1 files changed, 1 insertions, 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