diff options
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 2 | ||||
| -rw-r--r-- | plugins/derive/g_derive.mlg (renamed from plugins/derive/g_derive.ml4) | 14 | ||||
| -rw-r--r-- | plugins/derive/plugin_base.dune | 5 |
3 files changed, 17 insertions, 4 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 8a55538bde..480819ebe1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -61,7 +61,7 @@ let start_deriving f suchthat lemma = | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> - opaque <> Vernacexpr.Transparent , f_def , lemma_def + opaque <> Proof_global.Transparent , f_def , lemma_def | _ -> assert false in (** The opacity of [f_def] is adjusted to be [false], as it diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.mlg index a59324149c..df4b647642 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.mlg @@ -8,13 +8,21 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Stdarg +} + DECLARE PLUGIN "derive_plugin" -let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) +{ + +let classify_derive_command _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) + +} -VERNAC COMMAND EXTEND Derive CLASSIFIED BY classify_derive_command +VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } | [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] -> - [ Derive.start_deriving f suchthat lemma ] + { Derive.start_deriving f suchthat lemma } END diff --git a/plugins/derive/plugin_base.dune b/plugins/derive/plugin_base.dune new file mode 100644 index 0000000000..ba9cd595ce --- /dev/null +++ b/plugins/derive/plugin_base.dune @@ -0,0 +1,5 @@ +(library + (name derive_plugin) + (public_name coq.plugins.derive) + (synopsis "Coq's derive plugin") + (libraries coq.plugins.ltac)) |