diff options
Diffstat (limited to 'plugins/derive/g_derive.mlg')
| -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 ee076f5ae3..d25b8fd01c 100644 --- a/plugins/derive/g_derive.mlg +++ b/plugins/derive/g_derive.mlg @@ -23,6 +23,6 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac } VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } -| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - { fun ~pstate -> Some (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) } +| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> + { Derive.(start_deriving f suchthat lemma) } END |