Merge PR #10673: [lemmas] Cleanup users of default proof information.

Ack-by: SkySkimmer
Reviewed-by: ppedrot

5 files changed, 13 insertions, 37 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ca33e4e757..7be049269c 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 570b72136c..6011af74e5 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1387,15 +1387,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
@@ -1456,11 +1448,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 d5f5656e1d..0a8c4e6b0f 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -371,10 +371,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 da14b6e979..c8cede1f84 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