Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

1 files changed, 2 insertions, 2 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 439b1a5c..c232ae31 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -49,13 +49,13 @@ let start_deriving f suchthat lemma =
           [suchthat], respectively. *)
       let (opaque,f_def,lemma_def) =
         match com with
-        | Admitted -> Errors.error"Admitted isn't supported in Derive."
+        | Admitted _ -> Errors.error"Admitted isn't supported in Derive."
         | Proved (_,Some _,_) ->
             Errors.error"Cannot save a proof of Derive with an explicit name."
         | 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