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 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

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

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