aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/discharge.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/discharge.mli')
-rw-r--r--vernac/discharge.mli3
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/discharge.mli b/vernac/discharge.mli
index a0dabe2f4..c8c7e3b8b 100644
--- a/vernac/discharge.mli
+++ b/vernac/discharge.mli
@@ -11,5 +11,4 @@ open Entries
open Opaqueproof
val process_inductive :
- ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context)
- -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+ Lib.abstr_info -> work_list -> mutual_inductive_body -> mutual_inductive_entry