aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/derive
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-22 16:57:38 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-22 16:57:38 +0200
commit3c47248abc27aa9c64120db30dcb0d7bf945bc70 (patch)
tree0dd3a804e1924862390a7f78abc9a8a119127f9c /plugins/derive
parentceb68d1d643ac65f500e0201f61e73cf22e6e2fb (diff)
parent1bc1cba7a759a285131a3ed6ea8979716700b856 (diff)
Merge remote-tracking branch 'github/pr/283' into trunk
Was PR#283: Stylistic improvements in intf/decl_kinds.mli.
Diffstat (limited to 'plugins/derive')
-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