From 43d381ab20035f64ce2edea8639fcd9e1d0453bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:09:30 +0200
Subject: [declare] Move proof information to declare.

At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
---
 plugins/derive/derive.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/derive/derive.mli')

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
-- 
cgit v1.2.3