From 10b54c11e2db436ab077477fae862fe06e0d9395 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 19 Aug 2019 23:43:55 +0200 Subject: [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. --- plugins/funind/functional_principles_proofs.ml | 18 ++++-------------- plugins/funind/gen_principle.ml | 16 ++-------------- plugins/funind/recdef.ml | 6 ++---- vernac/classes.ml | 3 +-- vernac/obligations.ml | 7 ++++--- 5 files changed, 13 insertions(+), 37 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 diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 730ae48393..0a7757c616 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1369,15 +1369,7 @@ 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 info = Lemmas.Info.make - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decls.(IsProof Theorem)) () in - let lemma = Lemmas.start_lemma - ~name:lem_id - ~poly:false - ~info - !evd - typ in + let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ in let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma in let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in @@ -1434,11 +1426,7 @@ 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 = Lemmas.Info.make - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.(IsProof Theorem) () in - let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info - sigma (fst lemmas_types_infos.(i)) in + let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")") (proving_tac i))) lemma) in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index c62aa0cf6b..4c5eab1a9b 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1332,9 +1332,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type let lemma = build_proof env (Evd.from_env env) start_tac end_tac in Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None in - let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) - ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(IsProof Lemma)) - () in + let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in let lemma = Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info @@ -1376,7 +1374,7 @@ let com_terminate nb_args ctx hook = let start_proof env ctx tac_start tac_end = - let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(IsProof Lemma) () in + let info = Lemmas.Info.make ~hook () in let lemma = Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info diff --git a/vernac/classes.ml b/vernac/classes.ml index 075d89d0df..d3a591b203 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -373,10 +373,9 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t the refinement manually.*) let gls = List.rev (Evd.future_goals sigma) in let sigma = Evd.reset_future_goals sigma in - let scope = DeclareDef.Global Declare.ImportDefaultBehavior in let kind = Decls.(IsDefinition Instance) in let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in - let info = Lemmas.Info.make ~hook ~scope ~kind () in + let info = Lemmas.Info.make ~hook ~kind () in let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in (* spiwack: I don't know what to do with the status here. *) let lemma = diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 37fe0df0ee..c0b722af09 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -397,8 +397,8 @@ let deps_remaining obls deps = deps [] -let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(IsDefinition Definition)) -let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(IsProof Lemma)) +let goal_kind = Decls.(IsDefinition Definition) +let goal_proof_kind = Decls.(IsProof Lemma) let kind_of_obligation o = match o with @@ -487,7 +487,8 @@ let rec solve_obligation prg num tac = ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining)); in let obl = subst_deps_obl obls obl in - let scope, kind = kind_of_obligation (snd obl.obl_status) in + let scope = DeclareDef.(Global Declare.ImportNeedQualified) in + let kind = kind_of_obligation (snd obl.obl_status) in let evd = Evd.from_ctx prg.prg_ctx in let evd = Evd.update_sigma_env evd (Global.env ()) in let auto n oblset tac = auto_solve_obligations n ~oblset tac in -- cgit v1.2.3