From 7e577f93aca95d10584014e1d88dfbf314b74f9f Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 22 Jul 2014 17:55:00 +0200
Subject: Derive plugin: a more general interface.

Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def.
---
 plugins/Derive/derive.mli | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

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

diff --git a/plugins/Derive/derive.mli b/plugins/Derive/derive.mli
index 33f982bb68..5157c4a272 100644
--- a/plugins/Derive/derive.mli
+++ b/plugins/Derive/derive.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(** [start_deriving f init r lemma] starts a proof of [r init
-    ?x]. When the proof ends, [f] is defined as the value of [?x] and
-    [lemma] as the proof. *)
-val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr -> Names.Id.t -> unit
+(** [start_deriving f suchthat lemma] starts a proof of [suchthat]
+    (which can contain references to [f]) in the context extended by
+    [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
+    and [lemma] as the proof. *)
+val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> unit
-- 
cgit v1.2.3