From ec45ca30068a4b8bb4b2519b3839c96a729e0f20 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Mon, 8 Jul 2024 10:20:50 +0200
Subject: [PATCH 1/2] Remove generated files from archive and ignore them now

---
 .gitignore                       |   2 +
 template-coq/_PluginProject      | 252 -------------------------------
 template-coq/_TemplateCoqProject |  32 ----
 3 files changed, 2 insertions(+), 284 deletions(-)
 delete mode 100644 template-coq/_PluginProject
 delete mode 100644 template-coq/_TemplateCoqProject

diff --git a/.gitignore b/.gitignore
index 8d527267b..52d9f9507 100644
--- a/.gitignore
+++ b/.gitignore
@@ -249,6 +249,8 @@ checker/src/wf.mli
 /safechecker/_PluginProject
 /safechecker/_CoqProject
 /template-coq/_CoqProject
+/template-coq/_PluginProject
+/template-coq/_TemplateCoqProject
 /common/_CoqProject
 /safechecker/Makefile.safechecker.conf
 /safechecker/Makefile.safechecker
diff --git a/template-coq/_PluginProject b/template-coq/_PluginProject
deleted file mode 100644
index a51f3c4a7..000000000
--- a/template-coq/_PluginProject
+++ /dev/null
@@ -1,252 +0,0 @@
-# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh
--R ../utils/theories MetaCoq.Utils -R ../common/theories MetaCoq.Common
--I gen-src
--Q gen-src MetaCoq.Template
--R theories MetaCoq.Template
-META.coq-metacoq-template-ocaml
--I .
-
-# Generated Code by `ls -1 gen-src/*.ml gen-src/*.mli` in `template-coq/` after having compiled `Extraction.v`
-gen-src/all_Forall.ml
-gen-src/all_Forall.mli
-gen-src/ascii.ml
-gen-src/ascii.mli
-gen-src/ast0.ml
-gen-src/ast0.mli
-gen-src/astUtils.ml
-gen-src/astUtils.mli
-gen-src/ast_denoter.ml
-gen-src/ast_quoter.ml
-gen-src/basicAst.ml
-gen-src/basicAst.mli
-gen-src/basics.ml
-gen-src/basics.mli
-gen-src/binInt.ml
-gen-src/binInt.mli
-gen-src/binNat.ml
-gen-src/binNat.mli
-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
-gen-src/byte.mli
-gen-src/byte0.ml
-gen-src/byte0.mli
-gen-src/byteCompare.ml
-gen-src/byteCompare.mli
-gen-src/byteCompareSpec.ml
-gen-src/byteCompareSpec.mli
-gen-src/bytestring.ml
-gen-src/bytestring.mli
-gen-src/cRelationClasses.ml
-gen-src/cRelationClasses.mli
-gen-src/caml_byte.ml
-gen-src/caml_byte.mli
-gen-src/caml_bytestring.ml
-gen-src/caml_nat.ml
-gen-src/caml_nat.mli
-gen-src/carryType.ml
-gen-src/carryType.mli
-gen-src/classes0.ml
-gen-src/classes0.mli
-gen-src/common0.ml
-gen-src/common0.mli
-gen-src/compare_dec.ml
-gen-src/compare_dec.mli
-gen-src/config0.ml
-gen-src/config0.mli
-gen-src/coreTactics.ml
-gen-src/coreTactics.mli
-gen-src/datatypes.ml
-gen-src/datatypes.mli
-gen-src/decidableType.ml
-gen-src/decidableType.mli
-gen-src/decimal.ml
-gen-src/decimal.mli
-gen-src/denoter.ml
-gen-src/depElim.ml
-gen-src/depElim.mli
-gen-src/envMap.ml
-gen-src/envMap.mli
-gen-src/environment.ml
-gen-src/environment.mli
-gen-src/environmentTyping.ml
-gen-src/environmentTyping.mli
-gen-src/eqDec.ml
-gen-src/eqDec.mli
-gen-src/eqDecInstances.ml
-gen-src/eqDecInstances.mli
-gen-src/eqdepFacts.ml
-gen-src/eqdepFacts.mli
-gen-src/equalities.ml
-gen-src/equalities.mli
-gen-src/extractable.ml
-gen-src/extractable.mli
-gen-src/fMapAVL.ml
-gen-src/fMapAVL.mli
-gen-src/fMapFacts.ml
-gen-src/fMapFacts.mli
-gen-src/fMapInterface.ml
-gen-src/fMapInterface.mli
-gen-src/fMapList.ml
-gen-src/fMapList.mli
-gen-src/floatClass.ml
-gen-src/floatClass.mli
-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/kernames.ml
-gen-src/kernames.mli
-gen-src/liftSubst.ml
-gen-src/liftSubst.mli
-gen-src/list0.ml
-gen-src/list0.mli
-gen-src/logic0.ml
-gen-src/logic0.mli
-gen-src/logic1.ml
-gen-src/logic1.mli
-gen-src/logic2.ml
-gen-src/logic2.mli
-gen-src/mCCompare.ml
-gen-src/mCCompare.mli
-gen-src/mCFSets.ml
-gen-src/mCFSets.mli
-gen-src/mCList.ml
-gen-src/mCList.mli
-gen-src/mCMSets.ml
-gen-src/mCMSets.mli
-gen-src/mCOption.ml
-gen-src/mCOption.mli
-gen-src/mCPrelude.ml
-gen-src/mCPrelude.mli
-gen-src/mCProd.ml
-gen-src/mCProd.mli
-gen-src/mCReflect.ml
-gen-src/mCReflect.mli
-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
-gen-src/mCUtils.mli
-gen-src/mSetAVL.ml
-gen-src/mSetAVL.mli
-gen-src/mSetDecide.ml
-gen-src/mSetDecide.mli
-gen-src/mSetFacts.ml
-gen-src/mSetFacts.mli
-gen-src/mSetInterface.ml
-gen-src/mSetInterface.mli
-gen-src/mSetList.ml
-gen-src/mSetList.mli
-gen-src/mSetProperties.ml
-gen-src/mSetProperties.mli
-gen-src/monad_utils.ml
-gen-src/monad_utils.mli
-gen-src/nat0.ml
-gen-src/nat0.mli
-gen-src/noConfusion.ml
-gen-src/noConfusion.mli
-gen-src/number.ml
-gen-src/number.mli
-gen-src/orderedType0.ml
-gen-src/orderedType0.mli
-gen-src/orderedTypeAlt.ml
-gen-src/orderedTypeAlt.mli
-gen-src/orders.ml
-gen-src/orders.mli
-gen-src/ordersAlt.ml
-gen-src/ordersAlt.mli
-gen-src/ordersFacts.ml
-gen-src/ordersFacts.mli
-gen-src/ordersLists.ml
-gen-src/ordersLists.mli
-gen-src/ordersTac.ml
-gen-src/ordersTac.mli
-gen-src/peanoNat.ml
-gen-src/peanoNat.mli
-gen-src/plugin_core.ml
-gen-src/plugin_core.mli
-gen-src/pretty.ml
-gen-src/pretty.mli
-gen-src/primFloat.ml
-gen-src/primFloat.mli
-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/quoter.ml
-gen-src/reflect.ml
-gen-src/reflect.mli
-gen-src/reflectEq.ml
-gen-src/reflectEq.mli
-gen-src/reification.ml
-gen-src/relation.ml
-gen-src/relation.mli
-gen-src/run_extractable.ml
-gen-src/run_extractable.mli
-gen-src/signature.ml
-gen-src/signature.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
-gen-src/templateProgram.mli
-gen-src/termEquality.ml
-gen-src/termEquality.mli
-gen-src/tm_util.ml
-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/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
-
-theories/ExtractableLoader.v
diff --git a/template-coq/_TemplateCoqProject b/template-coq/_TemplateCoqProject
deleted file mode 100644
index 05f7e2517..000000000
--- a/template-coq/_TemplateCoqProject
+++ /dev/null
@@ -1,32 +0,0 @@
-# DO NOT EDIT THIS FILE: autogenerated from ./configure.sh
--R ../utils/theories MetaCoq.Utils -R ../common/theories MetaCoq.Common
--I src
--Q src MetaCoq.Template
--R theories MetaCoq.Template
-META.coq-metacoq-template-coq
--I .
-
-# the MetaCoq plugin
-src/tm_util.ml
-
-src/reification.ml
-src/quoter.ml
-src/denoter.ml
-src/constr_reification.ml
-src/constr_quoter.ml
-src/constr_denoter.ml
-
-src/g_template_coq.mlg
-src/template_coq.mlpack
-src/template_monad.mli
-src/template_monad.ml
-src/run_template_monad.mli
-src/run_template_monad.ml
-src/plugin_core.mli
-src/plugin_core.ml
-
-theories/Loader.v
-theories/All.v
-
-# A checker of well-formedness in MetaCoq and Coq
-theories/TemplateCheckWf.v

From 9cdb37bb79af1c37e2fba8b8cdd6f806108e4b85 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
Date: Mon, 8 Jul 2024 10:47:12 +0200
Subject: [PATCH 2/2] Fix translations due to new tString constructor

---
 erasure-plugin/clean_extraction.sh     | 2 +-
 pcuic/clean_extraction.sh              | 2 +-
 safechecker-plugin/clean_extraction.sh | 2 +-
 translations/param_binary.v            | 2 +-
 translations/param_original.v          | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/erasure-plugin/clean_extraction.sh b/erasure-plugin/clean_extraction.sh
index 4187f6ddc..562a941fa 100755
--- a/erasure-plugin/clean_extraction.sh
+++ b/erasure-plugin/clean_extraction.sh
@@ -9,7 +9,7 @@ fi
 
 shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
 
-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
 
 if [[ ! -f "src/metacoq_erasure_plugin.cmxs" ||
            "src/metacoq_erasure_plugin.cmxs" -ot "theories/Extraction.vo" ]]
diff --git a/pcuic/clean_extraction.sh b/pcuic/clean_extraction.sh
index d8ce50aff..7c5f8a0de 100755
--- a/pcuic/clean_extraction.sh
+++ b/pcuic/clean_extraction.sh
@@ -4,7 +4,7 @@ shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
 
 echo "Cleaning result of extraction"
 
-files=`cat ../template-coq/_PluginProject ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+files=`cat ../template-coq/_PluginProject.in ../checker/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
 
 cd src
 # Move extracted modules to build the certicoq compiler plugin
diff --git a/safechecker-plugin/clean_extraction.sh b/safechecker-plugin/clean_extraction.sh
index 44164597f..85e2f761a 100755
--- a/safechecker-plugin/clean_extraction.sh
+++ b/safechecker-plugin/clean_extraction.sh
@@ -9,7 +9,7 @@ fi
 
 shopt -s nullglob # make the for loop do nothnig when there is no *.ml* files
 
-files=`cat ../template-coq/_PluginProject | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
+files=`cat ../template-coq/_PluginProject.in | grep "^[^#].*mli\?$" | sed -e s/gen-src/src/`
 
 if [[ ! -f "src/metacoq_safechecker_plugin.cmxs" ||
            "src/metacoq_safechecker_plugin.cmxs" -ot "theories/Extraction.vo" ]]
diff --git a/translations/param_binary.v b/translations/param_binary.v
index ecf3c6be1..09c573065 100644
--- a/translations/param_binary.v
+++ b/translations/param_binary.v
@@ -145,7 +145,7 @@ Fixpoint tsl_rec1_app (app : list term) (E : tsl_table) (t : term) : term :=
   | tFix _ _ | tCoFix _ _ => todo "tsl"
   | tVar _ | tEvar _ _ => todo "tsl"
   | tLambda _ _ _ => tVar "impossible"
-  | tInt _ | tFloat _ | tArray _ _ _ _ => todo "tsl"
+  | tInt _ | tFloat _ | tArray _ _ _ _ | tString _ => todo "tsl"
   end
   in apply app t1
   end.
diff --git a/translations/param_original.v b/translations/param_original.v
index cbdcc3313..2173bcc0b 100644
--- a/translations/param_original.v
+++ b/translations/param_original.v
@@ -106,7 +106,7 @@ Fixpoint tsl_rec1_app (app : option term) (E : tsl_table) (t : term) : term :=
   | tFix _ _ | tCoFix _ _ => todo "tsl"
   | tVar _ | tEvar _ _ => todo "tsl"
   | tLambda _ _ _ => tVar "impossible"
-  | tInt _ | tFloat _ | tArray _ _ _ _ => todo "tsl"
+  | tInt _ | tFloat _ | tArray _ _ _ _ | tString _ => todo "tsl"
   end in
   match app with Some t' => mkApp t1 (t' {3 := tRel 1} {2 := tRel 0})
                | None => t1 end