diff options
| author | Arnaud Spiwack | 2014-07-22 17:55:00 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-07-23 17:52:46 +0200 |
| commit | 7e577f93aca95d10584014e1d88dfbf314b74f9f (patch) | |
| tree | dc4bc5197a1085098c756b76bc8b0c5356f38b00 /plugins/Derive/g_derive.ml4 | |
| parent | e143cffaeab1a294ca08a49443747c66bc963c29 (diff) | |
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.
Diffstat (limited to 'plugins/Derive/g_derive.ml4')
| -rw-r--r-- | plugins/Derive/g_derive.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
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 |