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

@@ -32,6 +32,9 @@ then
     # Remove extracted modules already linked in the template_coq plugin.
     echo "Removing:" $files
     rm -f $files
+
+    # confusion between Init.Wf and Program.Wf
+    sed -i.bak src/pCUICSafeChecker.ml -e 's/open Wf/open Wf0/'
 else
     echo "Extraction up-to date"
 fi

safechecker-plugin/src/metacoq_safechecker_plugin.mlpack

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

safechecker-plugin/theories/Extraction.v

@@ -48,6 +48,8 @@ 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.
 
+From Stdlib.Program Require Import Wf.
+Extraction Library Wf.
 Separate Extraction MakeOrderTac PCUICSafeChecker.typecheck_program
          infer_and_print_template_program_with_guard
          (* The following directives ensure separate extraction does not produce name clashes *)

safechecker/theories/PCUICTypeChecker.v

@@ -25,7 +25,7 @@ From MetaCoq.SafeChecker Require Import PCUICEqualityDec PCUICSafeReduce PCUICEr
 
 From Equations Require Import Equations.
 Require Import ssreflect ssrbool.
-Require Import Stdlib.Program.Program.
+From Stdlib Require Import Program.
 
 Local Set Keyed Unification.
 Set Equations Transparent.