diff options
Diffstat (limited to 'kernel/discharge.mli')
| -rw-r--r-- | kernel/discharge.mli | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/kernel/discharge.mli b/kernel/discharge.mli index 3e32a12c3c..1f06c5a734 100644 --- a/kernel/discharge.mli +++ b/kernel/discharge.mli @@ -10,8 +10,6 @@ open Declarations open Entries -open Opaqueproof val process_inductive : - Constr.named_context -> - Univ.Instance.t -> Univ.AUContext.t -> work_list -> mutual_inductive_body -> mutual_inductive_entry + Opaqueproof.cooking_info -> mutual_inductive_body -> mutual_inductive_entry |