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/recdef.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'plugins/funind/recdef.ml')

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
-- 
cgit v1.2.3