From 8338f05a214c2c85589e70df574436f476f00223 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 8 Jul 2024 10:47:12 +0200 Subject: [PATCH] Fix translations due to new tString constructor --- translations/param_binary.v | 2 +- translations/param_original.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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