From 0755a67e8b950f41fa3ae921fd358cef81d6b037 Mon Sep 17 00:00:00 2001 From: Oskar Goldhahn Date: Fri, 21 Nov 2025 16:00:48 +0100 Subject: [PATCH] fix outline error printing --- src/ecPrinting.ml | 8 ++++---- src/phl/ecPhlOutline.ml | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml index fd8171647..b37fbe228 100644 --- a/src/ecPrinting.ml +++ b/src/ecPrinting.ml @@ -2085,10 +2085,10 @@ and pp_form ppe fmt f = pp_form_r ppe (min_op_prec, `NonAssoc) fmt f and pp_expr ppe fmt e = - let f = match (EcEnv.Memory.get_active_ss ppe.PPEnv.ppe_env) with - | None -> form_of_expr e - | Some m -> (ss_inv_of_expr m e).inv in - pp_form ppe fmt f + let m = match (EcEnv.Memory.get_active_ss ppe.PPEnv.ppe_env) with + | None -> EcIdent.create "&hr" + | Some m -> m in + pp_form ppe fmt (ss_inv_of_expr m e).inv and pp_tuple_expr ppe fmt e = match e.e_node with diff --git a/src/phl/ecPhlOutline.ml b/src/phl/ecPhlOutline.ml index 9cfbbc8b2..1fd63d0bb 100644 --- a/src/phl/ecPhlOutline.ml +++ b/src/phl/ecPhlOutline.ml @@ -90,7 +90,7 @@ let process_outline info tc = | UnificationError UE_InvalidRetInstr -> tc_error !!tc "Outline: return instruction must be an assign. Perhaps consider using the alias variant using `~`." | UnificationError (UE_DifferentProgramLengths (s1, s2)) -> - tc_error !!tc "Outline: body's are different lengths\n%a ~ %a." (EcPrinting.pp_stmt ppe) s1 (EcPrinting.pp_stmt ppe) s2 + tc_error !!tc "Outline: bodies are different lengths\n%a ~ %a." (EcPrinting.pp_stmt ppe) s1 (EcPrinting.pp_stmt ppe) s2 | UnificationError (UE_InstrNotInLockstep (i1, i2))-> tc_error !!tc "outline: instructions not in sync\n%a ~ %a." (EcPrinting.pp_instr ppe) i1 (EcPrinting.pp_instr ppe) i2 | UnificationError (UE_LvNotInLockstep (_lv1, _lv2))->