Fix translations due to new tString constructor

MetaCoq · Jul 8, 2024 · 8338f05 · 8338f05
1 parent ec45ca3
commit 8338f05
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
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