diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-20 09:11:09 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-20 17:18:36 +0200 |
| commit | aa29c92dfa395e2f369e81bd72cef482cdf90c65 (patch) | |
| tree | fbffe7f83d1d76a21d39bf90b93d8f948aa42143 /plugins/funind/functional_principles_types.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 'plugins/funind/functional_principles_types.ml')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index cc699e5d3..4f5f167c2 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -288,7 +288,9 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin begin Lemmas.start_proof new_princ_name - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) + Decl_kinds.{ locality = Decl_kinds.Global; + polymorphic = Flags.is_universe_polymorphism (); + object_kind = Decl_kinds.Proof Decl_kinds.Theorem } !evd new_principle_type hook @@ -339,7 +341,9 @@ let generate_functional_principle (evd: Evd.evar_map ref) let evd',value = change_property_sort evd' s new_principle_type new_princ_name in let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in (* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *) - let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in + let ce = Declare.definition_entry ~polymorphic:(Flags.is_universe_polymorphism ()) + ~univs:(snd (Evd.universe_context evd')) value + in ignore( Declare.declare_constant name |