MetaCoq · proux01 · Jul 21, 2024
diff --git a/pcuic/theories/Bidirectional/BDStrengthening.v b/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

diff --git a/pcuic/theories/Syntax/PCUICDepth.v b/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.

diff --git a/pcuic/theories/Syntax/PCUICInduction.v b/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.

diff --git a/quotation/theories/ToPCUIC/Stdlib/Numbers.v b/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.

diff --git a/quotation/theories/ToTemplate/Stdlib/Numbers.v b/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.

diff --git a/safechecker-plugin/_PluginProject.in b/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

diff --git a/safechecker-plugin/clean_extraction.sh b/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
diff --git a/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack b/safechecker-plugin/src/metacoq_safechecker_plugin.mlpack
@@ -4,6 +4,7 @@ WGraph
 UGraph0
 Reflect
 MCProd
+Wf0
 
 Classes0
 Logic1

diff --git a/safechecker-plugin/theories/Extraction.v b/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 *)

diff --git a/safechecker/theories/PCUICTypeChecker.v b/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.

diff --git a/template-coq/Makefile b/template-coq/Makefile
@@ -74,14 +74,7 @@ cleanplugin: Makefile.plugin
 	make -f Makefile.plugin clean
 
 PLUGIN_PROJECT_BLACKLIST := \
-	carryType \
-	coreTactics \
-	depElim \
-	floatClass \
-	init \
 	mCUint63 \
-	noConfusion \
-	wf \
 	#
 
 space := $(subst ,, )

diff --git a/template-coq/_PluginProject.in b/template-coq/_PluginProject.in
@@ -27,10 +27,6 @@ gen-src/binNums.ml
 gen-src/binNums.mli
 gen-src/binPos.ml
 gen-src/binPos.mli
-gen-src/binPosDef.ml
-gen-src/binPosDef.mli
-gen-src/decidableClass.mli
-gen-src/decidableClass.ml
 gen-src/bool.ml
 gen-src/bool.mli
 gen-src/byte.ml
@@ -64,6 +60,8 @@ gen-src/coreTactics.ml
 gen-src/coreTactics.mli
 gen-src/datatypes.ml
 gen-src/datatypes.mli
+gen-src/decidableClass.ml
+gen-src/decidableClass.mli
 gen-src/decidableType.ml
 gen-src/decidableType.mli
 gen-src/decimal.ml
@@ -101,20 +99,22 @@ gen-src/floatOps.ml
 gen-src/floatOps.mli
 gen-src/hexadecimal.ml
 gen-src/hexadecimal.mli
-# gen-src/hexadecimalString.ml
-# gen-src/hexadecimalString.mli
 gen-src/induction0.ml
 gen-src/induction0.mli
 gen-src/init.ml
 gen-src/init.mli
 gen-src/int0.ml
 gen-src/int0.mli
+gen-src/intDef.ml
+gen-src/intDef.mli
 gen-src/kernames.ml
 gen-src/kernames.mli
 gen-src/liftSubst.ml
 gen-src/liftSubst.mli
 gen-src/list0.ml
 gen-src/list0.mli
+gen-src/listDef.ml
+gen-src/listDef.mli
 gen-src/logic0.ml
 gen-src/logic0.mli
 gen-src/logic1.ml
@@ -141,10 +141,6 @@ gen-src/mCRelations.ml
 gen-src/mCRelations.mli
 gen-src/mCString.ml
 gen-src/mCString.mli
-gen-src/sint63.mli
-gen-src/sint63.ml
-gen-src/show.mli
-gen-src/show.ml
 # gen-src/mCUint63.ml
 # gen-src/mCUint63.mli
 gen-src/mCUtils.ml
@@ -165,6 +161,8 @@ gen-src/monad_utils.ml
 gen-src/monad_utils.mli
 gen-src/nat0.ml
 gen-src/nat0.mli
+gen-src/natDef.ml
+gen-src/natDef.mli
 gen-src/noConfusion.ml
 gen-src/noConfusion.mli
 gen-src/number.ml
@@ -187,6 +185,8 @@ gen-src/peanoNat.ml
 gen-src/peanoNat.mli
 gen-src/plugin_core.ml
 gen-src/plugin_core.mli
+gen-src/posDef.ml
+gen-src/posDef.mli
 gen-src/pretty.ml
 gen-src/pretty.mli
 gen-src/primFloat.ml
@@ -195,10 +195,10 @@ gen-src/primInt63.ml
 gen-src/primInt63.mli
 gen-src/primString.ml
 gen-src/primString.mli
-gen-src/primitive.ml
-gen-src/primitive.mli
 gen-src/primStringAxioms.ml
 gen-src/primStringAxioms.mli
+gen-src/primitive.ml
+gen-src/primitive.mli
 gen-src/quoter.ml
 gen-src/reflect.ml
 gen-src/reflect.mli
@@ -209,16 +209,18 @@ gen-src/relation.ml
 gen-src/relation.mli
 gen-src/run_extractable.ml
 gen-src/run_extractable.mli
+gen-src/show.ml
+gen-src/show.mli
 gen-src/signature.ml
 gen-src/signature.mli
+gen-src/sint63Axioms.ml
+gen-src/sint63Axioms.mli
 gen-src/specFloat.ml
 gen-src/specFloat.mli
 gen-src/specif.ml
 gen-src/specif.mli
 gen-src/string0.ml
 gen-src/string0.mli
-gen-src/sumbool.ml
-gen-src/sumbool.mli
 gen-src/templateEnvMap.ml
 gen-src/templateEnvMap.mli
 gen-src/templateProgram.ml
@@ -230,20 +232,12 @@ gen-src/transform.ml
 gen-src/transform.mli
 gen-src/typing0.ml
 gen-src/typing0.mli
-gen-src/uint0.ml
-gen-src/uint0.mli
+gen-src/uint63Axioms.ml
+gen-src/uint63Axioms.mli
 gen-src/universes0.ml
 gen-src/universes0.mli
 gen-src/wf.ml
 gen-src/wf.mli
-gen-src/zArith_dec.ml
-gen-src/zArith_dec.mli
-gen-src/zbool.ml
-gen-src/zbool.mli
-gen-src/zeven.ml
-gen-src/zeven.mli
-gen-src/zpower.ml
-gen-src/zpower.mli
 
 gen-src/metacoq_template_plugin.mlpack
 

diff --git a/template-coq/gen-src/metacoq_template_plugin.mlpack b/template-coq/gen-src/metacoq_template_plugin.mlpack
@@ -7,16 +7,21 @@ Hexadecimal
 Numeral0
 Nat0
 Caml_nat
+ListDef
 List0
 PeanoNat
 Specif
 Basics
 BinPosDef
 BinNums
 BinPos
+PosDef
 BinNat
+NatDef
 BinInt
+IntDef
 PrimInt63
+Uint63Axioms
 Uint0
 Int63
 Byte
@@ -77,6 +82,7 @@ FloatOps
 PrimString
 PrimStringAxioms
 MCString
+Sint63Axioms
 Sint63
 Show
 MCUtils