From 43d381ab20035f64ce2edea8639fcd9e1d0453bc Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:09:30 +0200
Subject: [declare] Move proof information to declare.

At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
---
 plugins/derive/derive.ml                       |  9 ++++----
 plugins/derive/derive.mli                      |  2 +-
 plugins/extraction/extract_env.ml              |  4 ++--
 plugins/funind/functional_principles_proofs.ml |  5 ++--
 plugins/funind/gen_principle.ml                | 12 +++++-----
 plugins/funind/gen_principle.mli               |  2 +-
 plugins/funind/recdef.ml                       | 32 +++++++++++++-------------
 plugins/funind/recdef.mli                      |  2 +-
 plugins/ltac/extratactics.mlg                  |  4 ++--
 plugins/ltac/g_ltac.mlg                        |  2 +-
 plugins/ltac/rewrite.ml                        |  6 ++---
 plugins/ltac/rewrite.mli                       |  4 ++--
 12 files changed, 42 insertions(+), 42 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e5665c59b8..633d5dfe3b 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -15,7 +15,7 @@ open Context.Named.Declaration
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
     and [lemma] as the proof. *)
-let start_deriving f suchthat name : Lemmas.t =
+let start_deriving f suchthat name : Declare.Proof.t =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -40,8 +40,7 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let info = Lemmas.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
+  let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
   let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
-  Lemmas.pf_map (Declare.Proof.map_proof begin fun p ->
-    Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
-  end) lemma
+  Declare.Proof.map lemma ~f:(fun p ->
+      Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index ef94c7e78f..06e7dacd36 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -16,4 +16,4 @@ val start_deriving
   :  Names.Id.t
   -> Constrexpr.constr_expr
   -> Names.Id.t
-  -> Lemmas.t
+  -> Declare.Proof.t
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a0627dbe63..39c6c4ea54 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -729,13 +729,13 @@ let extract_and_compile l =
 (* Show the extraction of the current ongoing proof *)
 let show_extraction ~pstate =
   init ~inner:true false false;
-  let prf = Declare.Proof.get_proof pstate in
+  let prf = Declare.Proof.get pstate in
   let sigma, env = Declare.get_current_context pstate in
   let trms = Proof.partial_proof prf in
   let extr_term t =
     let ast, ty = extract_constr env sigma t in
     let mp = Lib.current_mp () in
-    let l = Label.of_id (Declare.Proof.get_proof_name pstate) in
+    let l = Label.of_id (Declare.Proof.get_name pstate) in
     let fake_ref = GlobRef.ConstRef (Constant.make2 mp l) in
     let decl = Dterm (fake_ref, ast, ty) in
     print_one_decl [] mp decl
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b864b18887..652f942cb9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -856,9 +856,10 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   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 lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
   let () =
-    Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
+    Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
+      ~idopt:None
   in
   evd
 
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 608155eb71..2336689a66 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1520,10 +1520,10 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let typ, _ = lemmas_types_infos.(i) 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
+            fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
           let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+            Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
               ~idopt:None
           in
           let finfo =
@@ -1586,7 +1586,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           in
           let lemma =
             fst
-              (Lemmas.by
+              (Declare.by
                  (Proofview.V82.tactic
                     (observe_tac
                        ("prove completeness (" ^ Id.to_string f_id ^ ")")
@@ -1594,7 +1594,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                  lemma)
           in
           let () =
-            Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent
+            Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
               ~idopt:None
           in
           let finfo =
@@ -1769,7 +1769,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt
     using_lemmas args ret_type body
 
 let do_generate_principle_aux pconstants on_error register_built
-    interactive_proof fixpoint_exprl : Lemmas.t option =
+    interactive_proof fixpoint_exprl : Declare.Proof.t option =
   List.iter
     (fun {Vernacexpr.notations} ->
       if not (List.is_empty notations) then
@@ -2155,7 +2155,7 @@ let make_graph (f_ref : GlobRef.t) =
 
 (* *************** statically typed entrypoints ************************* *)
 
-let do_generate_principle_interactive fixl : Lemmas.t =
+let do_generate_principle_interactive fixl : Declare.Proof.t =
   match do_generate_principle_aux [] warning_error true true fixl with
   | Some lemma -> lemma
   | None ->
diff --git a/plugins/funind/gen_principle.mli b/plugins/funind/gen_principle.mli
index 3c04d6cb7d..28751c4501 100644
--- a/plugins/funind/gen_principle.mli
+++ b/plugins/funind/gen_principle.mli
@@ -12,7 +12,7 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
 
 val do_generate_principle_interactive :
-  Vernacexpr.fixpoint_expr list -> Lemmas.t
+  Vernacexpr.fixpoint_expr list -> Declare.Proof.t
 
 val do_generate_principle : Vernacexpr.fixpoint_expr list -> unit
 val make_graph : Names.GlobRef.t -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9b2d9c4815..f92d4c6a72 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,7 +58,7 @@ let declare_fun name kind ?univs value =
     (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
+  Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent ~idopt:None
 
 let def_of_const t =
   match Constr.kind t with
@@ -1343,7 +1343,7 @@ let whole_start concl_tac nb_args is_mes func input_type relation rec_arg_num :
     g
 
 let get_current_subgoals_types pstate =
-  let p = Declare.Proof.get_proof pstate in
+  let p = Declare.Proof.get pstate in
   let Proof.{goals = sgs; sigma; _} = Proof.data p in
   (sigma, List.map (Goal.V82.abstract_type sigma) sgs)
 
@@ -1405,7 +1405,7 @@ let clear_goals sigma =
   List.map clear_goal
 
 let build_new_goal_type lemma =
-  let sigma, sub_gls_types = Lemmas.pf_fold get_current_subgoals_types lemma in
+  let sigma, sub_gls_types = get_current_subgoals_types lemma in
   (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
   let sub_gls_types = clear_goals sigma sub_gls_types in
   (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *)
@@ -1423,7 +1423,7 @@ let is_opaque_constant c =
 let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     (gls_type, decompose_and_tac, nb_goal) =
   (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
-  let current_proof_name = Lemmas.pf_fold Declare.Proof.get_proof_name lemma in
+  let current_proof_name = Declare.Proof.get_name lemma in
   let name =
     match goal_name with
     | Some s -> s
@@ -1488,18 +1488,18 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                      [Hints.Hint_db.empty TransparentState.empty false] ]))
     in
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
-    Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
+    Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None
   in
-  let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () 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
   in
   let lemma =
     if Indfun_common.is_strict_tcc () then
-      fst @@ Lemmas.by (Proofview.V82.tactic tclIDTAC) lemma
+      fst @@ Declare.by (Proofview.V82.tactic tclIDTAC) lemma
     else
       fst
-      @@ Lemmas.by
+      @@ Declare.by
            (Proofview.V82.tactic (fun g ->
                 tclTHEN decompose_and_tac
                   (tclORELSE
@@ -1521,27 +1521,26 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                   g))
            lemma
   in
-  if Lemmas.(pf_fold Declare.Proof.get_open_goals) lemma = 0 then (
-    defined lemma; None )
+  if Declare.Proof.get_open_goals lemma = 0 then (defined lemma; None)
   else Some lemma
 
 let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
     fonctional_ref input_type relation rec_arg_num thm_name using_lemmas nb_args
     ctx hook =
   let start_proof env ctx tac_start tac_end =
-    let info = Lemmas.Info.make ~hook () in
+    let info = Declare.Info.make ~hook () in
     let lemma =
       Lemmas.start_lemma ~name:thm_name ~poly:false (*FIXME*) ~info ctx
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
     in
     let lemma =
       fst
-      @@ Lemmas.by
+      @@ Declare.by
            (New.observe_tac (fun _ _ -> str "starting_tac") tac_start)
            lemma
     in
     fst
-    @@ Lemmas.by
+    @@ Declare.by
          (Proofview.V82.tactic
             (observe_tac
                (fun _ _ -> str "whole_start")
@@ -1608,7 +1607,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   in
   let lemma =
     fst
-    @@ Lemmas.by
+    @@ Declare.by
          (Proofview.V82.tactic
             (start_equation f_ref terminate_ref (fun x ->
                  prove_eq
@@ -1642,7 +1641,8 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   in
   let _ =
     Flags.silently
-      (fun () -> Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None)
+      (fun () ->
+        Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None)
       ()
   in
   ()
@@ -1651,7 +1651,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
 
 let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
     type_of_f r rec_arg_num eq generate_induction_principle using_lemmas :
-    Lemmas.t option =
+    Declare.Proof.t option =
   let open Term in
   let open Constr in
   let open CVars in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 4e5146e37c..2612f2b63e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -25,4 +25,4 @@ val recursive_definition :
       -> EConstr.constr
       -> unit)
   -> Constrexpr.constr_expr list
-  -> Lemmas.t option
+  -> Declare.Proof.t option
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index ffb597d4cb..40c64a1c26 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -918,7 +918,7 @@ END
 VERNAC COMMAND EXTEND GrabEvars STATE proof
 | [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
+  -> { fun ~pstate -> Declare.Proof.map ~f:(fun p -> Proof.V82.grab_evars p) pstate }
 END
 
 (* Shelves all the goals under focus. *)
@@ -950,7 +950,7 @@ END
 VERNAC COMMAND EXTEND Unshelve STATE proof
 | [ "Unshelve" ]
   => { classify_as_proofstep }
-  -> { fun ~pstate -> Declare.Proof.map_proof (fun p  -> Proof.unshelve p) pstate  }
+  -> { fun ~pstate -> Declare.Proof.map ~f:(fun p  -> Proof.unshelve p) pstate  }
 END
 
 (* Gives up on the goals under focus: the goals are considered solved,
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 996f6b3eb3..114acaa412 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -363,7 +363,7 @@ let print_info_trace =
 
 let vernac_solve ~pstate n info tcom b =
   let open Goal_select in
-  let pstate, status = Declare.Proof.map_fold_proof_endline (fun etac p ->
+  let pstate, status = Declare.Proof.map_fold_endline ~f:(fun etac p ->
       let with_end_tac = if b then Some etac else None in
       let global = match n with SelectAll | SelectList _ -> true | _ -> false in
       let info = Option.append info (print_info_trace ()) in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bc8d61258..e784d6e682 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1978,7 +1978,7 @@ let add_morphism_as_parameter atts m n : unit =
        (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst);
   declare_projection n instance_id cst
 
-let add_morphism_interactive atts m n : Lemmas.t =
+let add_morphism_interactive atts m n : Declare.Proof.t =
   init_setoid ();
   let instance_id = add_suffix n "_Proper" in
   let env = Global.env () in
@@ -1996,11 +1996,11 @@ let add_morphism_interactive atts m n : Lemmas.t =
     | _ -> assert false
   in
   let hook = Declare.Hook.make hook in
-  let info = Lemmas.Info.make ~hook ~kind () in
+  let info = Declare.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
        let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
-       fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
+       fst (Declare.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
   init_setoid ();
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 1161c84e6a..60a66dd861 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -101,7 +101,7 @@ val add_setoid
   -> Id.t
   -> unit
 
-val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Lemmas.t
+val add_morphism_interactive : rewrite_attributes -> constr_expr -> Id.t -> Declare.Proof.t
 val add_morphism_as_parameter : rewrite_attributes -> constr_expr -> Id.t -> unit
 
 val add_morphism
@@ -110,7 +110,7 @@ val add_morphism
   -> constr_expr
   -> constr_expr
   -> Id.t
-  -> Lemmas.t
+  -> Declare.Proof.t
 
 val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
 
-- 
cgit v1.2.3


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/derive/derive.ml                       |  2 +-
 plugins/funind/functional_principles_proofs.ml |  4 +++-
 plugins/funind/gen_principle.ml                | 10 ++++++++--
 plugins/funind/recdef.ml                       | 10 +++++++---
 plugins/ltac/rewrite.ml                        |  2 +-
 5 files changed, 20 insertions(+), 8 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 633d5dfe3b..c4f7638fb9 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t =
   in
 
   let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
-  let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
+  let lemma = Declare.start_dependent_proof ~name ~poly ~info ~udecl:UState.default_univ_decl goals in
   Declare.Proof.map lemma ~f:(fun p ->
       Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
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 =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e784d6e682..914dc96648 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1999,7 +1999,7 @@ let add_morphism_interactive atts m n : Declare.Proof.t =
   let info = Declare.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
+       let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] ~udecl:UState.default_univ_decl evd morph in
        fst (Declare.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
-- 
cgit v1.2.3


From 1f121ebf2990dc25899f2f3eb138eddd147483cf Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 15 May 2020 02:42:38 +0200
Subject: [declare] Refactor constant information into a record.

This improves the interface, and allows even more sealing of the API.

This is yet work in progress.
---
 plugins/ltac/rewrite.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 914dc96648..67d09acfda 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1902,8 +1902,9 @@ let declare_projection name instance_id r =
   let types = Some (it_mkProd_or_LetIn typ ctx) in
   let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
+  let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in
   let _r : GlobRef.t =
-    Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+    Declare.declare_definition ~name ~info ~types ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
-- 
cgit v1.2.3


From a6d663c85d71b3cce007af23419e8030b8c5ac88 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 14:57:44 +0200
Subject: [declare] [api] Removal of duplicated type aliases.

---
 plugins/funind/functional_principles_proofs.ml |  2 +-
 plugins/funind/gen_principle.ml                | 24 ++++++++++++------------
 plugins/funind/recdef.ml                       | 12 +++++++-----
 plugins/ltac/rewrite.ml                        |  4 ++--
 4 files changed, 22 insertions(+), 20 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c0d7c1e8e6..6ec12db952 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -860,7 +860,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   in
   let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
   let () =
-    Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
+    Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
       ~idopt:None
   in
   evd
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 30069c9914..8a07c2109e 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -319,7 +319,7 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
     let entry = Declare.definition_entry ~univs ?types body in
     let (_ : Names.GlobRef.t) =
       Declare.declare_entry ~name:new_princ_name ~hook
-        ~scope:(Declare.Global Declare.ImportDefaultBehavior)
+        ~scope:(Locality.Global Locality.ImportDefaultBehavior)
         ~kind:Decls.(IsProof Theorem)
         ~impargs:[] ~uctx entry
     in
@@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl =
           Pp.(str "Body of Function must be given")
     in
     ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
-      ~scope:(Declare.Global Declare.ImportDefaultBehavior)
+      ~scope:(Locality.Global Locality.ImportDefaultBehavior)
       ~kind:Decls.Definition univs binders None body (Some rtype);
     let evd, rev_pconstants =
       List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
     (None, evd, List.rev rev_pconstants)
   | _ ->
     ComFixpoint.do_fixpoint
-      ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
+      ~scope:(Locality.Global Locality.ImportDefaultBehavior) ~poly:false
       fixpoint_exprl;
     let evd, rev_pconstants =
       List.fold_left
@@ -1370,12 +1370,12 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
       | None -> raise Not_found
       | Some finfos -> finfos
     in
-    let open Declare in
     match finfos.equation_lemma with
-    | None -> Transparent (* non recursive definition *)
+    | None -> Vernacexpr.Transparent (* non recursive definition *)
     | Some equation ->
-      if Declareops.is_opaque (Global.lookup_constant equation) then Opaque
-      else Transparent
+      if Declareops.is_opaque (Global.lookup_constant equation) then
+        Vernacexpr.Opaque
+      else Vernacexpr.Transparent
   in
   let body, typ, univs, _hook, sigma0 =
     try
@@ -1527,8 +1527,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
             fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
-              ~idopt:None
+            Declare.save_lemma_proved ~proof:lemma
+              ~opaque:Vernacexpr.Transparent ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
@@ -1600,8 +1600,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                  lemma)
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent
-              ~idopt:None
+            Declare.save_lemma_proved ~proof:lemma
+              ~opaque:Vernacexpr.Transparent ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
@@ -2205,7 +2205,7 @@ let build_scheme fas =
   List.iter2
     (fun (princ_id, _, _) (body, types, univs, opaque) ->
       let (_ : Constant.t) =
-        let opaque = if opaque = Declare.Opaque then true else false in
+        let opaque = if opaque = Vernacexpr.Opaque then true else false in
         let def_entry = Declare.definition_entry ~univs ~opaque ?types body in
         Declare.declare_constant ~name:princ_id
           ~kind:Decls.(IsProof Theorem)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 58ed3864bb..853a54592d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,7 +58,8 @@ let declare_fun name kind ?univs value =
     (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Declare.save_lemma_proved ~proof:lemma ~opaque:Declare.Transparent ~idopt:None
+  Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
+    ~idopt:None
 
 let def_of_const t =
   match Constr.kind t with
@@ -1414,11 +1415,12 @@ let build_new_goal_type lemma =
 
 let is_opaque_constant c =
   let cb = Global.lookup_constant c in
+  let open Vernacexpr in
   match cb.Declarations.const_body with
-  | Declarations.OpaqueDef _ -> Declare.Opaque
-  | Declarations.Undef _ -> Declare.Opaque
-  | Declarations.Def _ -> Declare.Transparent
-  | Declarations.Primitive _ -> Declare.Opaque
+  | Declarations.OpaqueDef _ -> Opaque
+  | Declarations.Undef _ -> Opaque
+  | Declarations.Def _ -> Transparent
+  | Declarations.Primitive _ -> Opaque
 
 let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     (gls_type, decompose_and_tac, nb_goal) =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 67d09acfda..0bf97fefa6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1900,7 +1900,7 @@ let declare_projection name instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let types = Some (it_mkProd_or_LetIn typ ctx) in
-  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in
   let _r : GlobRef.t =
@@ -1968,7 +1968,7 @@ let add_morphism_as_parameter atts m n : unit =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let poly = atts.polymorphic in
-  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Locality.Global Locality.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let evd, types = build_morphism_signature env evd m in
   let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
-- 
cgit v1.2.3


From b143d124e140628e5974da4af1b8a70a4d534598 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 16:30:20 +0200
Subject: [declare] Move udecl to Info structure.

---
 plugins/derive/derive.ml                       | 2 +-
 plugins/funind/functional_principles_proofs.ml | 2 +-
 plugins/funind/gen_principle.ml                | 5 ++---
 plugins/funind/recdef.ml                       | 7 +++----
 plugins/ltac/rewrite.ml                        | 2 +-
 5 files changed, 8 insertions(+), 10 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index c4f7638fb9..7779e4f4c7 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t =
   in
 
   let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
-  let lemma = Declare.start_dependent_proof ~name ~poly ~info ~udecl:UState.default_univ_decl goals in
+  let lemma = Declare.start_dependent_proof ~name ~poly ~info goals in
   Declare.Proof.map lemma ~f:(fun p ->
       Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 6ec12db952..2c85ae079f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -856,7 +856,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let info = Declare.Info.make () in
   let lemma =
     Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info
-      ~impargs:[] ~udecl:UState.default_univ_decl evd lemma_type
+      ~impargs:[] 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 8a07c2109e..a914cef6e4 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1520,8 +1520,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let typ, _ = lemmas_types_infos.(i) 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
+            Declare.start_proof ~name:lem_id ~poly:false ~info ~impargs:[] !evd
+              typ
           in
           let lemma =
             fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
@@ -1587,7 +1587,6 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let info = Declare.Info.make () in
           let lemma =
             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 853a54592d..9f36eada45 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1494,8 +1494,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 =
-    Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[]
-      ~udecl:UState.default_univ_decl sigma gls_type
+    Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
+      gls_type
   in
   let lemma =
     if Indfun_common.is_strict_tcc () then
@@ -1534,7 +1534,7 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
     let info = Declare.Info.make ~hook () in
     let lemma =
       Declare.start_proof ~name:thm_name ~poly:false (*FIXME*) ~info ctx
-        ~impargs:[] ~udecl:UState.default_univ_decl
+        ~impargs:[]
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
     in
     let lemma =
@@ -1608,7 +1608,6 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   let info = Declare.Info.make () in
   let lemma =
     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 =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 0bf97fefa6..0c1c763b64 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2000,7 +2000,7 @@ let add_morphism_interactive atts m n : Declare.Proof.t =
   let info = Declare.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] ~udecl:UState.default_univ_decl evd morph in
+       let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] evd morph in
        fst (Declare.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
-- 
cgit v1.2.3


From 030bb57d4b7e70d45379cab61903b75bf7a41b19 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 25 May 2020 16:43:01 +0200
Subject: [declare] Reify Proof.t API into the Proof module.

This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
---
 plugins/derive/derive.ml                       |  2 +-
 plugins/extraction/extract_env.ml              |  2 +-
 plugins/funind/functional_principles_proofs.ml |  9 +++++----
 plugins/funind/gen_principle.ml                | 16 ++++++++--------
 plugins/funind/recdef.ml                       | 24 +++++++++++-------------
 plugins/ltac/rewrite.ml                        |  4 ++--
 6 files changed, 28 insertions(+), 29 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 7779e4f4c7..d85d3bd744 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t =
   in
 
   let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
-  let lemma = Declare.start_dependent_proof ~name ~poly ~info goals in
+  let lemma = Declare.Proof.start_dependent ~name ~poly ~info goals in
   Declare.Proof.map lemma ~f:(fun p ->
       Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39c6c4ea54..af43c0517e 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -730,7 +730,7 @@ let extract_and_compile l =
 let show_extraction ~pstate =
   init ~inner:true false false;
   let prf = Declare.Proof.get pstate in
-  let sigma, env = Declare.get_current_context pstate in
+  let sigma, env = Declare.Proof.get_current_context pstate in
   let trms = Proof.partial_proof prf in
   let extr_term t =
     let ast, ty = extract_constr env sigma t in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2c85ae079f..79f311e282 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -855,13 +855,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
      constructing the lemma Ensures by: obvious i*)
   let info = Declare.Info.make () in
   let lemma =
-    Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info
+    Declare.Proof.start ~name:(mk_equation_id f_id) ~poly:false ~info
       ~impargs:[] evd lemma_type
   in
-  let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
+  let lemma, _ =
+    Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
+  in
   let () =
-    Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
-      ~idopt:None
+    Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
   in
   evd
 
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index a914cef6e4..50ce783579 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1520,15 +1520,15 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let typ, _ = lemmas_types_infos.(i) in
           let info = Declare.Info.make () in
           let lemma =
-            Declare.start_proof ~name:lem_id ~poly:false ~info ~impargs:[] !evd
+            Declare.Proof.start ~name:lem_id ~poly:false ~info ~impargs:[] !evd
               typ
           in
           let lemma =
-            fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
+            fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma
-              ~opaque:Vernacexpr.Transparent ~idopt:None
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
+              ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
@@ -1586,12 +1586,12 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let lem_id = mk_complete_id f_id in
           let info = Declare.Info.make () in
           let lemma =
-            Declare.start_proof ~name:lem_id ~poly:false sigma ~info ~impargs:[]
+            Declare.Proof.start ~name:lem_id ~poly:false sigma ~info ~impargs:[]
               (fst lemmas_types_infos.(i))
           in
           let lemma =
             fst
-              (Declare.by
+              (Declare.Proof.by
                  (Proofview.V82.tactic
                     (observe_tac
                        ("prove completeness (" ^ Id.to_string f_id ^ ")")
@@ -1599,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                  lemma)
           in
           let () =
-            Declare.save_lemma_proved ~proof:lemma
-              ~opaque:Vernacexpr.Transparent ~idopt:None
+            Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
+              ~idopt:None
           in
           let finfo =
             match find_Function_infos (fst f_as_constant) with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9f36eada45..5a188ca82b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,8 +58,7 @@ let declare_fun name kind ?univs value =
     (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
-    ~idopt:None
+  Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
 
 let def_of_const t =
   match Constr.kind t with
@@ -1490,19 +1489,19 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                      [Hints.Hint_db.empty TransparentState.empty false] ]))
     in
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
-    Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None
+    Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
   in
   let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
-    Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
+    Declare.Proof.start ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
       gls_type
   in
   let lemma =
     if Indfun_common.is_strict_tcc () then
-      fst @@ Declare.by (Proofview.V82.tactic tclIDTAC) lemma
+      fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma
     else
       fst
-      @@ Declare.by
+      @@ Declare.Proof.by
            (Proofview.V82.tactic (fun g ->
                 tclTHEN decompose_and_tac
                   (tclORELSE
@@ -1533,18 +1532,18 @@ 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 =
-      Declare.start_proof ~name:thm_name ~poly:false (*FIXME*) ~info ctx
+      Declare.Proof.start ~name:thm_name ~poly:false (*FIXME*) ~info ctx
         ~impargs:[]
         (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
     in
     let lemma =
       fst
-      @@ Declare.by
+      @@ Declare.Proof.by
            (New.observe_tac (fun _ _ -> str "starting_tac") tac_start)
            lemma
     in
     fst
-    @@ Declare.by
+    @@ Declare.Proof.by
          (Proofview.V82.tactic
             (observe_tac
                (fun _ _ -> str "whole_start")
@@ -1607,12 +1606,12 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   let equation_lemma_type = subst1 f_constr equation_lemma_type in
   let info = Declare.Info.make () in
   let lemma =
-    Declare.start_proof ~name:eq_name ~poly:false evd ~info ~impargs:[]
+    Declare.Proof.start ~name:eq_name ~poly:false evd ~info ~impargs:[]
       (EConstr.of_constr equation_lemma_type)
   in
   let lemma =
     fst
-    @@ Declare.by
+    @@ Declare.Proof.by
          (Proofview.V82.tactic
             (start_equation f_ref terminate_ref (fun x ->
                  prove_eq
@@ -1646,8 +1645,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   in
   let _ =
     Flags.silently
-      (fun () ->
-        Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None)
+      (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
       ()
   in
   ()
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 0c1c763b64..405fe7b844 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2000,8 +2000,8 @@ let add_morphism_interactive atts m n : Declare.Proof.t =
   let info = Declare.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] evd morph in
-       fst (Declare.by (Tacinterp.interp tac) lemma)) ()
+       let lemma = Declare.Proof.start ~name:instance_id ~poly ~info ~impargs:[] evd morph in
+       fst (Declare.Proof.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
   init_setoid ();
-- 
cgit v1.2.3


From ea8b9e060dfba9cc8706677e29c26dabaaa87551 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 22 Jun 2020 20:42:39 +0200
Subject: [declare] Improve organization of proof/constant information.

We unify information about constants so it is shared among all the
paths [interactive, NI, obligations].

IMHO the current setup looks pretty good, with information split into
a per-constant record `CInfo.t` and variables affecting mutual
definitions at once, which live in `Info.t`.

Main information outside our `Info` record is `opaque`, which is
provided at different moments in several cases.

There are a few nits regarding interactive proofs, which will go away
in the next commits.
---
 plugins/derive/derive.ml                       |  5 +++--
 plugins/funind/functional_principles_proofs.ml |  6 +++---
 plugins/funind/gen_principle.ml                | 12 +++++-------
 plugins/funind/recdef.ml                       | 25 +++++++++++++------------
 plugins/ltac/rewrite.ml                        | 10 ++++++----
 5 files changed, 30 insertions(+), 28 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index d85d3bd744..27df963e98 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -40,7 +40,8 @@ let start_deriving f suchthat name : Declare.Proof.t =
                 TNil sigma))))))
   in
 
-  let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
-  let lemma = Declare.Proof.start_dependent ~name ~poly ~info goals in
+  let info = Declare.Info.make ~poly ~kind () in
+  let proof_ending = Declare.Proof_ending.(End_derive {f; name}) in
+  let lemma = Declare.Proof.start_dependent ~name ~info ~proof_ending goals in
   Declare.Proof.map lemma ~f:(fun p ->
       Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 79f311e282..afe89aef6e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -854,10 +854,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 =
-    Declare.Proof.start ~name:(mk_equation_id f_id) ~poly:false ~info
-      ~impargs:[] evd lemma_type
+  let cinfo =
+    Declare.CInfo.make ~name:(mk_equation_id f_id) ~typ:lemma_type ()
   in
+  let lemma = Declare.Proof.start ~cinfo ~info evd in
   let lemma, _ =
     Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
   in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 50ce783579..0cd5df12f7 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1519,10 +1519,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let lem_id = mk_correct_id f_id in
           let typ, _ = lemmas_types_infos.(i) in
           let info = Declare.Info.make () in
-          let lemma =
-            Declare.Proof.start ~name:lem_id ~poly:false ~info ~impargs:[] !evd
-              typ
-          in
+          let cinfo = Declare.CInfo.make ~name:lem_id ~typ () in
+          let lemma = Declare.Proof.start ~cinfo ~info !evd in
           let lemma =
             fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
@@ -1585,10 +1583,10 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
             i*)
           let lem_id = mk_complete_id f_id in
           let info = Declare.Info.make () in
-          let lemma =
-            Declare.Proof.start ~name:lem_id ~poly:false sigma ~info ~impargs:[]
-              (fst lemmas_types_infos.(i))
+          let cinfo =
+            Declare.CInfo.make ~name:lem_id ~typ:(fst lemmas_types_infos.(i)) ()
           in
+          let lemma = Declare.Proof.start ~cinfo sigma ~info in
           let lemma =
             fst
               (Declare.Proof.by
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5a188ca82b..92eb85ffd8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1492,10 +1492,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
   in
   let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
-  let lemma =
-    Declare.Proof.start ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
-      gls_type
-  in
+  let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type () in
+  let lemma = Declare.Proof.start ~cinfo ~info sigma in
   let lemma =
     if Indfun_common.is_strict_tcc () then
       fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma
@@ -1530,12 +1528,13 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
     fonctional_ref input_type relation rec_arg_num thm_name using_lemmas nb_args
     ctx hook =
   let start_proof env ctx tac_start tac_end =
-    let info = Declare.Info.make ~hook () in
-    let lemma =
-      Declare.Proof.start ~name:thm_name ~poly:false (*FIXME*) ~info ctx
-        ~impargs:[]
-        (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
+    let cinfo =
+      Declare.CInfo.make ~name:thm_name
+        ~typ:(EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
+        ()
     in
+    let info = Declare.Info.make ~hook () in
+    let lemma = Declare.Proof.start ~cinfo ~info ctx in
     let lemma =
       fst
       @@ Declare.Proof.by
@@ -1605,10 +1604,12 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
   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 =
-    Declare.Proof.start ~name:eq_name ~poly:false evd ~info ~impargs:[]
-      (EConstr.of_constr equation_lemma_type)
+  let cinfo =
+    Declare.CInfo.make ~name:eq_name
+      ~typ:(EConstr.of_constr equation_lemma_type)
+      ()
   in
+  let lemma = Declare.Proof.start ~cinfo evd ~info in
   let lemma =
     fst
     @@ Declare.Proof.by
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 405fe7b844..f16d0717df 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1902,9 +1902,10 @@ let declare_projection name instance_id r =
   let types = Some (it_mkProd_or_LetIn typ ctx) in
   let kind, opaque, scope = Decls.(IsDefinition Definition), false, Locality.Global Locality.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
-  let info = Declare.CInfo.make ~scope ~kind ~opaque ~impargs ~udecl ~poly () in
+  let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in
+  let info = Declare.Info.make ~scope ~kind ~udecl ~poly () in
   let _r : GlobRef.t =
-    Declare.declare_definition ~name ~info ~types ~body sigma
+    Declare.declare_definition ~cinfo ~info ~opaque ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
@@ -1997,10 +1998,11 @@ let add_morphism_interactive atts m n : Declare.Proof.t =
     | _ -> assert false
   in
   let hook = Declare.Hook.make hook in
-  let info = Declare.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Declare.Proof.start ~name:instance_id ~poly ~info ~impargs:[] evd morph in
+       let cinfo = Declare.CInfo.make ~name:instance_id ~typ:morph () in
+       let info = Declare.Info.make ~poly ~hook ~kind () in
+       let lemma = Declare.Proof.start ~cinfo ~info evd in
        fst (Declare.Proof.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
-- 
cgit v1.2.3


From 4a2c8653c0b2f5e73db769a8ea6bf79b76086524 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 23 Jun 2020 22:36:22 +0200
Subject: [declare] Merge remaining obligations bits into Declare

This allows us to remove a large chunk of the internal API, and is the
pre-requisite to get rid of [Proof_ending], and even more refactoring
on the declare path.
---
 plugins/ltac/g_obligations.mlg | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 498b33d1a8..81ee6ed5bb 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -28,7 +28,7 @@ let () =
   let tac = Proofview.tclBIND (Proofview.tclUNIT ()) begin fun () ->
     snd (get_default_tactic ())
   end in
-  Obligations.default_tactic := tac
+  Declare.Obls.default_tactic := tac
 
 let with_tac f tac =
   let env = Genintern.empty_glob_sign (Global.env ()) in
@@ -78,10 +78,10 @@ GRAMMAR EXTEND Gram
 
 {
 
-open Obligations
+open Declare.Obls
 
-let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
-let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
+let obligation obl tac = with_tac (fun t -> obligation obl t) tac
+let next_obligation obl tac = with_tac (fun t -> next_obligation obl t) tac
 
 let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
 
-- 
cgit v1.2.3


From d9dca86f798ce11861f1a4715763cad1aae28e5a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 23 Jun 2020 22:47:53 +0200
Subject: [declare] Remove Proof_ending from the public API

This completes the refactoring [for now] of the core `Declare`
interface, and will allow much internal refactoring in the future.

In particular, we remove the low-level Proof_ending type, and instead
introduce higher-level constructors for the several declare users.

Future PRs will change the internal representation of proof handling
to better enforce some invariants that should hold for specific
proofs.
---
 plugins/derive/derive.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 27df963e98..027064b75f 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -41,7 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t =
   in
 
   let info = Declare.Info.make ~poly ~kind () in
-  let proof_ending = Declare.Proof_ending.(End_derive {f; name}) in
-  let lemma = Declare.Proof.start_dependent ~name ~info ~proof_ending goals in
+  let lemma = Declare.Proof.start_derive ~name ~f ~info goals in
   Declare.Proof.map lemma ~f:(fun p ->
       Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
-- 
cgit v1.2.3


From a5a65ddcf0e476384c827cdf2445bc554eae825a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 24 Jun 2020 14:22:57 +0200
Subject: [declare] Return list of declared global in Proof.save

This is needed in rewriter as to avoid hack; indeed it makes sense to
propagate this information to the callers of save.
---
 plugins/funind/functional_principles_proofs.ml |  2 +-
 plugins/funind/gen_principle.ml                |  4 ++--
 plugins/funind/recdef.ml                       | 10 ++++++++--
 3 files changed, 11 insertions(+), 5 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index afe89aef6e..2151ad7873 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -861,7 +861,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let lemma, _ =
     Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
   in
-  let () =
+  let (_ : _ list) =
     Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
   in
   evd
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 0cd5df12f7..167cf37026 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1524,7 +1524,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let lemma =
             fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
-          let () =
+          let (_ : GlobRef.t list) =
             Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
               ~idopt:None
           in
@@ -1596,7 +1596,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                        (proving_tac i)))
                  lemma)
           in
-          let () =
+          let (_ : _ list) =
             Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
               ~idopt:None
           in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 92eb85ffd8..884792cc15 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,7 +58,10 @@ let declare_fun name kind ?univs value =
     (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+  let (_ : _ list) =
+    Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+  in
+  ()
 
 let def_of_const t =
   match Constr.kind t with
@@ -1489,7 +1492,10 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                      [Hints.Hint_db.empty TransparentState.empty false] ]))
     in
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
-    Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+    let (_ : _ list) =
+      Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+    in
+    ()
   in
   let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
   let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type () in
-- 
cgit v1.2.3