From 17ba18d81e5fe3dc153b1c12ac1b8daeb5474d48 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 2 May 2019 06:10:29 +0200 Subject: [lemmas] Turn Lemmas.info into a proper type with constructor. Lemmas.info was a bit out of hand, as well as the parameters to the `start_*` family. Most of the info is not needed and should hopefully remain constrained to special cases, most callers only set the hook, and obligations should be better served by a `start_obligation` function soon. --- plugins/funind/functional_principles_proofs.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ce3b5a82d6..9c593a55d8 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -994,10 +994,11 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (*i The next call to mk_equation_id is valid since we are constructing the lemma Ensures by: obvious i*) - (mk_equation_id f_id) - Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem) - evd - lemma_type + ~name:(mk_equation_id f_id) + ~kind:Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem) + + evd + lemma_type in let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in -- cgit v1.2.3 From fd2d2a8178d78e441fb3191cf112ed517dc791af Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 May 2019 05:33:10 +0200 Subject: [proof] Remove duplicated universe polymorphic from decl_kinds This information is already present on `Proof.t`, so we extract it form there. Moreover, this information is essential to the lower-level proof, as opposed to the "kind" information which is only relevant to the vernac layer; we will move it thus to its proper layer in subsequent commits. --- plugins/funind/functional_principles_proofs.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 9c593a55d8..c37e6f7402 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -995,8 +995,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num Ensures by: obvious i*) ~name:(mk_equation_id f_id) - ~kind:Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem) - + ~poly:false + ~kind:(Decl_kinds.(Global ImportDefaultBehavior, Proof Theorem)) evd lemma_type in -- cgit v1.2.3 From 8b903319eae4d645f9385e8280d04d18a4f3a2bc Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Jun 2019 06:09:24 +0200 Subject: [lemmas] [proof] Split proof kinds into per-layer components. We split `{goal,declaration,assumption}_kind` into their components. This makes sense as each part of this triple is handled by a different layer, namely: - `polymorphic` status: necessary for the lower engine layers; - `locality`: only used in `vernac` top-level constants - `kind`: merely used for cosmetic purposes [could indeed be removed / pushed upwards] We also profit from this refactoring to add some named parameters to the top-level definition API which is quite parameter-hungry. More refactoring is possible and will come in further commits, in particular this is a step towards unifying the definition / lemma save path. --- plugins/funind/functional_principles_proofs.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c37e6f7402..0d3c7b365f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -990,13 +990,17 @@ 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:Decl_kinds.(Global ImportDefaultBehavior) + ~kind:(Decl_kinds.Proof Decl_kinds.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 - ~kind:(Decl_kinds.(Global ImportDefaultBehavior, Proof Theorem)) + ~info evd lemma_type in -- cgit v1.2.3 From b2aae7ba35a90e695d34f904c74f5156385344a9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 6 Jun 2019 13:21:48 +0200 Subject: [api] Move `locality` from `library` to `vernac`. This datatype does belong to this layer. --- plugins/funind/functional_principles_proofs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind/functional_principles_proofs.ml') diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 0d3c7b365f..a904b81d81 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -991,7 +991,7 @@ 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:Decl_kinds.(Global ImportDefaultBehavior) + ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in let lemma = Lemmas.start_lemma -- cgit v1.2.3