diff options
Diffstat (limited to 'vernac/discharge.mli')
| -rw-r--r-- | vernac/discharge.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/discharge.mli b/vernac/discharge.mli index 18d1b6776..3845c04a1 100644 --- a/vernac/discharge.mli +++ b/vernac/discharge.mli @@ -11,4 +11,5 @@ open Entries open Opaqueproof val process_inductive : - Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry + ((Term.constr, Term.constr) Context.Named.pt * Univ.abstract_universe_context) + -> work_list -> mutual_inductive_body -> mutual_inductive_entry |