Fix translations due to new tString constructor

MetaCoq · Jul 9, 2024 · 9cdb37b · 9cdb37b
1 parent ec45ca3
commit 9cdb37b
Show file tree

Hide file tree

Showing 5 changed files with 5 additions and 5 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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