From 3d2988ea5b94429e8141add1b1c6db4c3d4453b2 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Wed, 20 May 2026 16:40:08 +0200 Subject: [PATCH] emit proper error message when typing `={pvar}` in a single sided context --- src/ecTyping.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 3a4c27a77..c1305741f 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -3241,7 +3241,9 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt = let do1 = function | GVvar x -> - let ml, mr = oget (EcEnv.Memory.get_active_ts env) in + let ml, mr = match (EcEnv.Memory.get_active_ts env) with + | Some (ml, mr) -> ml, mr + | None -> tyerror f.pl_loc env (UnexpectedGoalShape GSE_ExpectedTwoSided) in let x1 = lookup ml (qual (om |> omap fst) x) in let x2 = lookup mr (qual (om |> omap snd) x) in unify_or_fail env ue x.pl_loc ~expct:x1.f_ty x2.f_ty;