diff options
| author | Pierre-Marie Pédrot | 2015-02-15 18:17:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-15 18:17:04 +0100 |
| commit | d7691de7184b4cdcfd48fd762011569cde5523c5 (patch) | |
| tree | 9c9e14226b070fc2a5cf4c216c4f8c634de20855 /plugins/derive | |
| parent | eed12bddc3e6f6f9192c909a8b8f82859080f3a1 (diff) | |
| parent | aed3c876d422f4dcc0296fd4949148c697f37b1d (diff) | |
Merge branch 'v8.5'
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 439b1a5c01..a77b552e01 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -55,7 +55,7 @@ let start_deriving f suchthat lemma = | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> - opaque , f_def , lemma_def + opaque <> Vernacexpr.Transparent , f_def , lemma_def | _ -> assert false in (** The opacity of [f_def] is adjusted to be [false], as it |