Adapt to rocq-prover/rocq#21467. (#189)

Author: ppedrot

src/Rewriter/Util/plugins/rewriter_build.ml.v92

@@ -62,7 +62,7 @@ let rewriter_heuristic_process_rules_proofs env sigma ~poly rules_proofs =
   let rules_proofs_with_args = mkApp (rules_proofs_with_args, [|rules_proofs_ty; rules_proofs|]) in
   let uctx = Evd.evar_universe_context sigma in
   let (rules_proofs_sig, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
-    Declare.build_by_tactic env ~uctx ~poly ~typ:rules_proofs_with_args rules_proofs_with_args_tac in
+    Subproof.build_by_tactic env ~uctx ~poly ~typ:rules_proofs_with_args rules_proofs_with_args_tac in
   let sigma = Evd.from_ctx uctx in (* XXX IS THIS RIGHT? *)
   let rules_proofs_sig = EConstr.of_constr rules_proofs_sig in
   (sigma, projT2_skip_cast env sigma rules_proofs_sig)
@@ -83,7 +83,7 @@ let rewriter_scrape_data env sigma ~poly (rules_proofs : EConstr.t) (extra : ECo
   let scraped_data_ty = mkApp (scraped_data_with_args, [|rules_ty; rules_proofs; extra_ty; extra|]) in
   let uctx = Evd.evar_universe_context sigma in
   let (scraped_data, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
-    Declare.build_by_tactic env ~uctx ~poly ~typ:scraped_data_ty scraped_data_with_args_tac in
+    Subproof.build_by_tactic env ~uctx ~poly ~typ:scraped_data_ty scraped_data_with_args_tac in
   let sigma = Evd.from_ctx uctx in (* XXX IS THIS RIGHT? *)
   (sigma, EConstr.of_constr scraped_data)
 
@@ -98,7 +98,7 @@ let rewriter_emit_inductives sigma ~poly (scraped_data : EConstr.t) (base_name :
   let (sigma, raw_ident_elim_with_args) = Evd.fresh_global env sigma (r_raw_ident_elim_with_args ()) in
   let uctx = Evd.evar_universe_context sigma in
   let (base_elim, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
-    Declare.build_by_tactic env ~uctx ~poly ~typ:base_elim_ty base_elim_with_args_tac in
+    Subproof.build_by_tactic env ~uctx ~poly ~typ:base_elim_ty base_elim_with_args_tac in
   let sigma = Evd.from_ctx uctx in (* XXX IS THIS RIGHT? *)
   let base_name = name_or base_name "base" in
   let (sigma, base) = make_inductive_from_elim sigma (Some base_name) (EConstr.of_constr base_elim) in
@@ -109,11 +109,11 @@ let rewriter_emit_inductives sigma ~poly (scraped_data : EConstr.t) (base_name :
   let raw_ident_elim_ty = mkApp (raw_ident_elim_with_args, [|scraped_data;base|]) in
   let uctx = Evd.evar_universe_context sigma in
   let (ident_elim, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
-    Declare.build_by_tactic env ~uctx ~poly ~typ:ident_elim_ty ident_elim_with_args_tac in
+    Subproof.build_by_tactic env ~uctx ~poly ~typ:ident_elim_ty ident_elim_with_args_tac in
   let (pattern_ident_elim, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
-    Declare.build_by_tactic env ~uctx ~poly ~typ:pattern_ident_elim_ty pattern_ident_elim_with_args_tac in
+    Subproof.build_by_tactic env ~uctx ~poly ~typ:pattern_ident_elim_ty pattern_ident_elim_with_args_tac in
   let (raw_ident_elim, _maybe_type, _univs, _uses_unsafe_tactic, uctx) =
-    Declare.build_by_tactic env ~uctx ~poly ~typ:raw_ident_elim_ty raw_ident_elim_with_args_tac in
+    Subproof.build_by_tactic env ~uctx ~poly ~typ:raw_ident_elim_ty raw_ident_elim_with_args_tac in
   let sigma = Evd.from_ctx uctx in (* XXX IS THIS RIGHT? *)
   let ident_name = name_or ident_name "ident" in
   let (sigma, ident) = make_inductive_from_elim sigma (Some ident_name) (EConstr.of_constr ident_elim) in