diff options
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 |