diff options
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/g_derive.mlg | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg index d25b8fd01c..526989fdf3 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -22,7 +22,7 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac } -VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } -| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> +VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof +| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> { Derive.(start_deriving f suchthat lemma) } END |