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/g_derive.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/Derive/g_derive.ml4')

diff --git a/plugins/Derive/g_derive.ml4 b/plugins/Derive/g_derive.ml4
index 9137c3d282..0721c675fa 100644
--- a/plugins/Derive/g_derive.ml4
+++ b/plugins/Derive/g_derive.ml4
@@ -11,6 +11,6 @@
 let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater)
 
 VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command
-| [ "Derive" ident(f) "From" constr(init) "Upto" constr(r) "As" ident(lemma) ] ->
-     [ Derive.start_deriving f init r lemma ]
+| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
+     [ Derive.start_deriving f suchthat lemma ]
 END
-- 
cgit v1.2.3