Merge PR #12372: [declare] Refactor constant information into a record.

Reviewed-by: SkySkimmer

5 files changed, 19 insertions, 16 deletions

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/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,[]))
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bc8d61258..f16d0717df 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1900,10 +1900,12 @@ 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 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 ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+    Declare.declare_definition ~cinfo ~info ~opaque ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
@@ -1967,7 +1969,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
@@ -1978,7 +1980,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 +1998,12 @@ 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
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
-       fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
+       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 =
   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