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". --- proofs/pfedit.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/pfedit.mli') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index f2f4b11ed..aa01969b7 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -169,7 +169,7 @@ val build_constant_by_tactic : types -> unit Proofview.tactic -> Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context -val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> +val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?polymorphic:polymorphic -> types -> unit Proofview.tactic -> constr * bool * Evd.evar_universe_context -- cgit v1.2.3