fix outline error printing

Author: oskgo

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

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))->