aboutsummaryrefslogtreecommitdiff
path: root/plugins/derive/derive.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/derive/derive.mli')
-rw-r--r--plugins/derive/derive.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index ef94c7e78f..06e7dacd36 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -16,4 +16,4 @@ val start_deriving
: Names.Id.t
-> Constrexpr.constr_expr
-> Names.Id.t
- -> Lemmas.t
+ -> Declare.Proof.t