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 /plugins/funind/invfun.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/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index c8b4e48337..6d042b3a49 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -832,7 +832,9 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( let (typ,_) = lemmas_types_infos.(i) in Lemmas.start_proof lem_id - (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 typ (Lemmas.mk_hook (fun _ _ -> ())); @@ -893,10 +895,13 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( Ensures by: obvious i*) let lem_id = mk_complete_id f_id in - Lemmas.start_proof lem_id - (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma - (fst lemmas_types_infos.(i)) - (Lemmas.mk_hook (fun _ _ -> ())); + Lemmas.start_proof lem_id + Decl_kinds.{ locality = Decl_kinds.Global; + polymorphic = Flags.is_universe_polymorphism (); + object_kind = Decl_kinds.Proof Decl_kinds.Theorem } + sigma + (fst lemmas_types_infos.(i)) + (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i)))) ; |