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