diff options
| author | Pierre-Marie Pédrot | 2018-05-24 01:05:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-05-24 01:05:09 +0200 |
| commit | 9df6df865fc71ed9840fc569d3aa3cc7cf4750aa (patch) | |
| tree | 8965b5d9bc37bc7d0be341dc311fef6df43c3616 /plugins/derive | |
| parent | b74d9500e5943317f1baf4f36b3d979d40f6105f (diff) | |
| parent | b4b515c2e61bc6ea662b48e84eb319ec8252b07d (diff) | |
Merge PR #6515: [api] Move `Vernacexpr` to parsing.
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/derive.ml | 2 |
1 files changed, 1 insertions, 1 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 |