Adapt to rocq-prover/rocq#19530

Author: proux01

pcuic/theories/Bidirectional/BDStrengthening.v

@@ -11,7 +11,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICGlobalEnv
 From MetaCoq.PCUIC Require Import BDTyping BDToPCUIC BDFromPCUIC.
 
 Require Import ssreflect ssrbool.
-Require Import Coq.Program.Equality.
+From Coq.Program Require Import Equality.
 
 Ltac case_inequalities :=
   match goal with

pcuic/theories/Syntax/PCUICDepth.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect Program Lia BinPos Arith.Compare_dec Bool.
+From Coq Require Import ssreflect Program Lia BinPos Compare_dec Bool.
 From MetaCoq.Utils Require Import utils LibHypsNaming.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICSize PCUICInduction.
 From Coq Require Import List.

pcuic/theories/Syntax/PCUICInduction.v

@@ -1,5 +1,5 @@
 (* Distributed under the terms of the MIT license. *)
-From Coq Require Import ssreflect Program Lia BinPos Arith.Compare_dec Bool.
+From Coq Require Import ssreflect Program Lia BinPos Compare_dec Bool.
 From MetaCoq.Utils Require Import utils LibHypsNaming.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICCases PCUICSize.
 From Coq Require Import List.

quotation/theories/ToPCUIC/Stdlib/Numbers.v

@@ -2,7 +2,7 @@ From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts
      Cyclic.Int63.PrimInt63 Cyclic.Int63.Uint63
      Cyclic.Abstract.CyclicAxioms
      Cyclic.Abstract.DoubleType
-     Cyclic.Abstract.CarryType
+     Cyclic.Int63.CarryType
 .
 
 From Coq Require Import ZArith.

quotation/theories/ToTemplate/Stdlib/Numbers.v

@@ -2,7 +2,7 @@ From Coq.Numbers Require Import BinNums DecimalFacts HexadecimalFacts
      Cyclic.Int63.PrimInt63 Cyclic.Int63.Uint63
      Cyclic.Abstract.CyclicAxioms
      Cyclic.Abstract.DoubleType
-     Cyclic.Abstract.CarryType
+     Cyclic.Int63.CarryType
 .
 From Coq Require Import ZArith.
 From MetaCoq.Quotation.ToTemplate Require Import Stdlib.Init.

safechecker-plugin/_PluginProject.in

@@ -13,6 +13,8 @@ src/uGraph0.ml
 src/uGraph0.mli
 src/wGraph.ml
 src/wGraph.mli
+src/wf0.ml
+src/wf0.mli
 
 # From PCUIC
 src/pCUICPrimitive.mli

safechecker-plugin/clean_extraction.sh

@@ -29,6 +29,11 @@ then
     done
     cd ..
 
+    # confusion between Init.Wf and Program.Wf
+    mv src/wf.ml src/wf0.ml
+    mv src/wf.mli src/wf0.mli
+    sed -i.bak src/pCUICSafeChecker.ml -e 's/open Wf/open Wf0/'
+
     # Remove extracted modules already linked in the template_coq plugin.
     echo "Removing:" $files
     rm -f $files

safechecker-plugin/src/metacoq_safechecker_plugin.mlpack

@@ -4,6 +4,7 @@ WGraph
 UGraph0
 Reflect
 MCProd
+Wf0
 
 Classes0
 Logic1

safechecker-plugin/theories/Extraction.v

@@ -48,7 +48,7 @@ Next Obligation. eapply fake_abstract_guard_impl_properties. Qed.
 Definition infer_and_print_template_program_with_guard {cf} {nor} :=
   @SafeTemplateChecker.infer_and_print_template_program cf nor fake_abstract_guard_impl.
 
-Separate Extraction MakeOrderTac PCUICSafeChecker.typecheck_program
+Separate Extraction Wf.Fix_sub MakeOrderTac PCUICSafeChecker.typecheck_program
          infer_and_print_template_program_with_guard
          (* The following directives ensure separate extraction does not produce name clashes *)
          Stdlib.Strings.String UnivSubst PCUICPretty.

safechecker/theories/PCUICSafeChecker.v

@@ -106,7 +106,7 @@ Definition gcs_equal x y : Prop :=
 
 
 (** It otherwise tries [auto with *], very bad idea. *)
-Ltac Stdlib.Program.Tactics.program_solve_wf ::=
+Ltac Corelib.Program.Tactics.program_solve_wf ::=
   match goal with
   | |- @Wf.well_founded _ _ => auto with subterm wf
   | |- ?T => match type of T with