diff options
| author | Emilio Jesus Gallego Arias | 2019-08-19 23:43:55 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-23 23:41:08 +0200 |
| commit | 10b54c11e2db436ab077477fae862fe06e0d9395 (patch) | |
| tree | 3cd3892d568e1a9c71b883a638c25455ff62bc5d /plugins/funind/functional_principles_proofs.ml | |
| parent | b0a9cbeaf0530533008aa99246164b2bad896c5a (diff) | |
[lemmas] Cleanup users of default proof information.
We remove calls of `Lemmas.Info.make` that where using the default
parameters, as this is mostly dead code now.
This brings into question quite a few things, in particular, the
uneven support of `scope` attributes by different commands / plugins.
We don't attempt to solve that yet, hopefully the ongoing constant
saving path refactoring will be able to take care of these
inconsistencies.
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 18 |
1 files changed, 4 insertions, 14 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5a939b4adf..78b53b1007 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -920,20 +920,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num ] in (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *) - let info = Lemmas.Info.make - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decls.(IsProof Theorem)) () in - - let lemma = Lemmas.start_lemma - (*i The next call to mk_equation_id is valid since we are constructing the lemma - Ensures by: obvious - i*) - ~name:(mk_equation_id f_id) - ~poly:false - ~info - evd - lemma_type - in + + (*i The next call to mk_equation_id is valid since we are + constructing the lemma Ensures by: obvious i*) + let lemma = Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type in let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in evd |