From aa29c92dfa395e2f369e81bd72cef482cdf90c65 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 20 Sep 2016 09:11:09 +0200 Subject: Stylistic improvements in intf/decl_kinds.mli. We get rid of tuples containing booleans (typically for universe polymorphism) by replacing them with records. The previously common idom: if pi2 kind (* polymorphic *) then ... else ... becomes: if kind.polymorphic then ... else ... To make the construction and destruction of these records lightweight, the labels of boolean arguments for universe polymorphism are now usually also called "polymorphic". --- plugins/derive/derive.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'plugins/derive') 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 -- cgit v1.2.3