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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/leminv.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index d80e862418..c7b8e6cc05 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -233,7 +233,7 @@ let inversion_scheme env sigma t sort dep_option inv_op = let add_inversion_lemma name env sigma t sort dep inv_op = let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in - let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ()) + let entry = definition_entry ~polymorphic:(Flags.use_polymorphic_flag ()) ~univs:(snd ctx) invProof in let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in () diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9d0e9f0842..86c0b9dd5c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4888,7 +4888,9 @@ let anon_id = Id.of_string "anonymous" let tclABSTRACT name_op tac = let open Proof_global in - let default_gk = (Global, false, Proof Theorem) in + let default_gk = + { locality = Global; polymorphic = false; object_kind = Proof Theorem } + in let s, gk = match name_op with | Some s -> (try let _, gk, _ = current_proof_statement () in s, gk |