diff options
| author | Maxime Dénès | 2016-09-20 09:11:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-20 17:18:36 +0200 |
| commit | aa29c92dfa395e2f369e81bd72cef482cdf90c65 (patch) | |
| tree | fbffe7f83d1d76a21d39bf90b93d8f948aa42143 /toplevel/class.ml | |
| parent | 424de98770e1fd8c307a7cd0053c268a48532463 (diff) | |
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".
Diffstat (limited to 'toplevel/class.ml')
| -rw-r--r-- | toplevel/class.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml index 0dc7990143..9582015a08 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -180,7 +180,7 @@ let error_not_transparent source = user_err ~hdr:"build_id_coercion" (pr_class source ++ str " must be a transparent constant.") -let build_id_coercion idf_opt source poly = +let build_id_coercion idf_opt source ~polymorphic = let env = Global.env () in let sigma = Evd.from_env env in let sigma, vs = match source with @@ -221,7 +221,7 @@ let build_id_coercion idf_opt source poly = in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry - (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma)) + (definition_entry ~types:typ_f ~polymorphic ~univs:(snd (Evd.universe_context sigma)) ~inline:true (mkCast (val_f, DEFAULTcast, typ_f))) in let decl = (constr_entry, IsDefinition IdentityCoercion) in |