Fix translations due to new tString constructor

Author: mattam82

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" ]]

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

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" ]]

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.

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