aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/derive/derive.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/derive/derive.ml')
-rw-r--r--plugins/derive/derive.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e39d17b52..12fd8359a 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -22,7 +22,10 @@ let start_deriving f suchthat lemma =
let env = Global.env () in
let sigma = Evd.from_env env in
- let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in
+ let kind = Decl_kinds.{ locality = Global;
+ polymorphic = false;
+ object_kind = DefinitionBody Definition }
+ in
(** create a sort variable for the type of [f] *)
(* spiwack: I don't know what the rigidity flag does, picked the one