From 671004aac9f9d3b70ef41f81e7b3ea8f190971ec Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:20:24 +0200
Subject: [declare] Remove Lemmas module

The module is now a stub. We choose to be explicit on the parameters
for now, this will improve in next commits with the refactoring of
proof / constant information.
---
 plugins/funind/functional_principles_proofs.ml |  4 +++-
 plugins/funind/gen_principle.ml                | 10 ++++++++--
 plugins/funind/recdef.ml                       | 10 +++++++---
 3 files changed, 18 insertions(+), 6 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 652f942cb9..c0d7c1e8e6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -853,8 +853,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 
   (*i The next call to mk_equation_id is valid since we are
      constructing the lemma Ensures by: obvious i*)
+  let info = Declare.Info.make () in
   let lemma =
-    Lemmas.start_lemma ~name:(mk_equation_id f_id) ~poly:false evd lemma_type
+    Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info
+      ~impargs:[] ~udecl:UState.default_univ_decl evd lemma_type
   in
   let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
   let () =
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 2336689a66..30069c9914 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1518,7 +1518,11 @@ 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 lemma = Lemmas.start_lemma ~name:lem_id ~poly:false !evd typ in
+          let info = Declare.Info.make () in
+          let lemma =
+            Declare.start_proof ~name:lem_id ~poly:false ~info ~impargs:[]
+              ~udecl:UState.default_univ_decl !evd typ
+          in
           let lemma =
             fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
@@ -1580,8 +1584,10 @@ 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 = Declare.Info.make () in
           let lemma =
-            Lemmas.start_lemma ~name:lem_id ~poly:false sigma
+            Declare.start_proof ~name:lem_id ~poly:false sigma ~info ~impargs:[]
+              ~udecl:UState.default_univ_decl
               (fst lemmas_types_infos.(i))
           in
           let lemma =
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f92d4c6a72..58ed3864bb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1492,7 +1492,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
   in
   let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
-    Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
+    Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[]
+      ~udecl:UState.default_univ_decl sigma gls_type
   in
   let lemma =
     if Indfun_common.is_strict_tcc () then
@@ -1530,7 +1531,8 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
   let start_proof env ctx tac_start tac_end =
     let info = Declare.Info.make ~hook () in
     let lemma =
-      Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info ctx
+      Declare.start_proof ~name:thm_name ~poly:false (*FIXME*) ~info ctx
+        ~impargs:[] ~udecl:UState.default_univ_decl
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
     in
     let lemma =
@@ -1601,8 +1603,10 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   let evd = Evd.from_ctx uctx in
   let f_constr = constr_of_monomorphic_global f_ref in
   let equation_lemma_type = subst1 f_constr equation_lemma_type in
+  let info = Declare.Info.make () in
   let lemma =
-    Lemmas.start_lemma ~name:eq_name ~poly:false evd
+    Declare.start_proof ~name:eq_name ~poly:false evd ~info ~impargs:[]
+      ~udecl:UState.default_univ_decl
       (EConstr.of_constr equation_lemma_type)
   in
   let lemma =
-- 
cgit v1.2.3