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.
---
 vernac/classes.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/classes.mli')

diff --git a/vernac/classes.mli b/vernac/classes.mli
index 1b6deb3b28..07695b5bef 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -36,7 +36,7 @@ val new_instance_interactive
   -> ?hook:(GlobRef.t -> unit)
   -> Vernacexpr.hint_info_expr
   -> (bool * constr_expr) option
-  -> Id.t * Lemmas.t
+  -> Id.t * Declare.Proof.t
 
 val new_instance
   :  ?global:bool (** Not global by default. *)
-- 
cgit v1.2.3