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.
---
 vernac/classes.ml     | 3 +--
 vernac/obligations.ml | 7 ++++---
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'vernac')

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