From 671004aac9f9d3b70ef41f81e7b3ea8f190971ec Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 25 May 2020 14:20:24 +0200 Subject: [declare] Remove Lemmas module The module is now a stub. We choose to be explicit on the parameters for now, this will improve in next commits with the refactoring of proof / constant information. --- plugins/derive/derive.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 4 +++- plugins/funind/gen_principle.ml | 10 ++++++-- plugins/funind/recdef.ml | 10 +++++--- plugins/ltac/rewrite.ml | 2 +- vernac/classes.ml | 2 +- vernac/lemmas.ml | 30 ------------------------ vernac/lemmas.mli | 32 -------------------------- vernac/obligations.ml | 2 +- vernac/vernac.mllib | 1 - 10 files changed, 22 insertions(+), 73 deletions(-) delete mode 100644 vernac/lemmas.ml delete mode 100644 vernac/lemmas.mli diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 633d5dfe3b..c4f7638fb9 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t = in let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in - let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in + let lemma = Declare.start_dependent_proof ~name ~poly ~info ~udecl:UState.default_univ_decl goals in Declare.Proof.map lemma ~f:(fun p -> Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 652f942cb9..c0d7c1e8e6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -853,8 +853,10 @@ 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*) + let info = Declare.Info.make () in let lemma = - Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type + Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info + ~impargs:[] ~udecl:UState.default_univ_decl evd lemma_type in let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in let () = diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 2336689a66..30069c9914 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1518,7 +1518,11 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) i*) let lem_id = mk_correct_id f_id in let typ, _ = lemmas_types_infos.(i) in - let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ in + let info = Declare.Info.make () in + let lemma = + Declare.start_proof ~name:lem_id ~poly:false ~info ~impargs:[] + ~udecl:UState.default_univ_decl !evd typ + in let lemma = fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma in @@ -1580,8 +1584,10 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) Ensures by: obvious i*) let lem_id = mk_complete_id f_id in + let info = Declare.Info.make () in let lemma = - Lemmas.start_lemma ~name:lem_id ~poly:false sigma + Declare.start_proof ~name:lem_id ~poly:false sigma ~info ~impargs:[] + ~udecl:UState.default_univ_decl (fst lemmas_types_infos.(i)) in let lemma = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f92d4c6a72..58ed3864bb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1492,7 +1492,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name in let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in let lemma = - Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type + Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] + ~udecl:UState.default_univ_decl sigma gls_type in let lemma = if Indfun_common.is_strict_tcc () then @@ -1530,7 +1531,8 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes let start_proof env ctx tac_start tac_end = let info = Declare.Info.make ~hook () in let lemma = - Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info ctx + Declare.start_proof ~name:thm_name ~poly:false (*FIXME*) ~info ctx + ~impargs:[] ~udecl:UState.default_univ_decl (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in let lemma = @@ -1601,8 +1603,10 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref let evd = Evd.from_ctx uctx in let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in + let info = Declare.Info.make () in let lemma = - Lemmas.start_lemma ~name:eq_name ~poly:false evd + Declare.start_proof ~name:eq_name ~poly:false evd ~info ~impargs:[] + ~udecl:UState.default_univ_decl (EConstr.of_constr equation_lemma_type) in let lemma = diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e784d6e682..914dc96648 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1999,7 +1999,7 @@ let add_morphism_interactive atts m n : Declare.Proof.t = let info = Declare.Info.make ~hook ~kind () in Flags.silently (fun () -> - let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in + let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] ~udecl:UState.default_univ_decl evd morph in fst (Declare.by (Tacinterp.interp tac) lemma)) () let add_morphism atts binders m s n = diff --git a/vernac/classes.ml b/vernac/classes.ml index 973c6f8e7c..f7d8a4b42f 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -362,7 +362,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails! This is due to a bug in proof_global :( *) let termtype = Evarutil.nf_evar sigma termtype in - let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in + let lemma = Declare.start_proof ~name:id ~poly ~udecl ~info ~impargs sigma termtype in (* spiwack: I don't know what to do with the status here. *) let lemma = match term with diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml deleted file mode 100644 index 6fe9b7c257..0000000000 --- a/vernac/lemmas.ml +++ /dev/null @@ -1,30 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* poly:bool - -> ?udecl:UState.universe_decl - -> ?info:Declare.Info.t - -> ?impargs:Impargs.manual_implicits - -> Evd.evar_map - -> EConstr.types - -> Declare.Proof.t - -val start_dependent_lemma - : name:Id.t - -> poly:bool - -> ?udecl:UState.universe_decl - -> ?info:Declare.Info.t - -> Proofview.telescope - -> Declare.Proof.t diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 05edb55760..62fdbf50ad 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -146,7 +146,7 @@ let rec solve_obligation prg num tac = in let info = Declare.Info.make ~proof_ending ~scope ~kind () in let poly = prg.prg_poly in - let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in + let lemma = Declare.start_proof ~name:obl.obl_name ~poly ~impargs:[] ~udecl:UState.default_univ_decl ~info evd (EConstr.of_constr obl.obl_type) in let lemma = fst @@ Declare.by !default_tactic lemma in let lemma = Option.cata (fun tac -> Declare.Proof.set_endline_tactic tac lemma) lemma tac in lemma diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 1cad052bce..c30703d734 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -20,7 +20,6 @@ ComHints Canonical RecLemmas Library -Lemmas ComCoercion Auto_ind_decl Indschemes -- cgit v1.2.3