[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.

5 files changed, 30 insertions, 28 deletions

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 =