From 5cd8e883c76b2386a356435efc35a6c8bb93f043 Mon Sep 17 00:00:00 2001 From: Wonho Date: Fri, 26 Jul 2024 16:59:27 +0900 Subject: [PATCH] Fix note in animation --- spectec/src/il2al/animate.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spectec/src/il2al/animate.ml b/spectec/src/il2al/animate.ml index 5aec64f518..c9e142c4ec 100644 --- a/spectec/src/il2al/animate.ml +++ b/spectec/src/il2al/animate.ml @@ -238,7 +238,7 @@ let rec pre_process prem = match prem.it with (* `C` |- `lhs` : `rhs` *) | [[]; [turnstile]; [colon]; []], TupE [_; lhs; rhs] when turnstile.it = Turnstile && colon.it = Colon -> - let typing_function_call = CallE (id, [ExpA lhs $ lhs.at]) $$ exp.at % exp.note in + let typing_function_call = CallE (id, [ExpA lhs $ lhs.at]) $$ exp.at % rhs.note in [ { prem with it=IfPr (CmpE (EqOp, typing_function_call, rhs) $$ exp.at % exp.note) } ] | _ -> [ prem ] )