From 43e403a676a1ce3e2bdd113ff45864b396f647b8 Mon Sep 17 00:00:00 2001
From: Lionel Blatter <lionel.blatter@mpi-sp.org>
Date: Mon, 23 Mar 2026 18:26:36 +0100
Subject: [PATCH] Merge the default optional postcondition for exception into
 the map of exceptions

---
 src/ecAst.ml           | 71 ++++++++++++++++--------------------------
 src/ecAst.mli          |  8 ++---
 src/ecCoreLib.ml       |  3 ++
 src/ecCoreLib.mli      |  3 ++
 src/ecPrinting.ml      | 28 ++++++++++++++---
 src/ecProofTyping.ml   | 13 ++++++--
 src/ecProofTyping.mli  |  7 ++---
 src/ecReduction.ml     | 26 ++++++----------
 src/ecSubst.ml         |  7 ++---
 src/ecTyping.ml        | 25 +++++++--------
 src/ecTyping.mli       |  2 +-
 src/phl/ecPhlCall.ml   | 12 +++----
 src/phl/ecPhlConseq.ml | 48 ++++++++++++++--------------
 src/phl/ecPhlFun.ml    |  4 +--
 src/phl/ecPhlWp.ml     | 17 +++++-----
 15 files changed, 139 insertions(+), 135 deletions(-)

diff --git a/src/ecAst.ml b/src/ecAst.ml
index 3c7ac5fcbe..b6d66ebdb9 100644
--- a/src/ecAst.ml
+++ b/src/ecAst.ml
@@ -294,7 +294,7 @@ and pr = {
 
 and exnpost = {
   main   : form;
-  exnmap : form Mp.t * form option;
+  exnmap : form Mp.t;
 }
 
 let map_ss_inv ?m (fn: form list -> form) (invs: ss_inv list): ss_inv =
@@ -565,20 +565,20 @@ let map_inv3 (fn: form -> form -> form -> form)
       failwith "incompatible invariants for map_inv3"
 
 (* ----------------------------------------------------------------- *)
-type 'a prepoe = 'a * ('a Mp.t * 'a option)
+type 'a prepoe = 'a * ('a Mp.t)
 
 module POE = struct
-  let mk (main : form) (exnmap : form Mp.t * form option) =
+  let mk (main : form) (exnmap : form Mp.t) =
     { main; exnmap; }
 
   let destruct (poe : exnpost) =
     (poe.main, poe.exnmap)
 
   let empty (f : form) : exnpost =
-    { main = f; exnmap = (Mp.empty, None); }
+    { main = f; exnmap = Mp.empty; }
 
-  let is_empty ({ exnmap = (m, dfl) } : exnpost) =
-    Option.is_none dfl && Mp.is_empty m
+  let is_empty ({ exnmap } : exnpost) =
+    Mp.is_empty exnmap
 
   let lift (f : ss_inv) =
     { hsi_m = f.m; hsi_inv = empty f.inv; }
@@ -586,12 +586,12 @@ module POE = struct
   let lower (f : hs_inv) =
     { m = f.hsi_m; inv = f.hsi_inv.main; }
 
-  let map (f : form -> form) ({ main; exnmap = (m, d) } : exnpost) : exnpost =
-    { main = f main; exnmap = (Mp.map f m, omap f d)}
+  let map (f : form -> form) ({ main; exnmap } : exnpost) : exnpost =
+    { main = f main; exnmap = Mp.map f exnmap}
 
   let map2_pre (f : 'a -> 'b -> 'c) (poe1 : 'a prepoe) (poe2 : 'b prepoe) : 'c prepoe =
-    let (main1, (map1, d1)) = poe1 in
-    let (main2, (map2, d2)) = poe2 in
+    let (main1, map1) = poe1 in
+    let (main2, map2) = poe2 in
 
     let merge (a : 'a option) (b : 'b option) =
       match a, b with
@@ -602,9 +602,8 @@ module POE = struct
 
     let main = f main1 main2 in
     let map  = Mp.merge (fun _ -> merge) map1 map2 in
-    let dfl  = merge d1 d2 in
 
-    (main, (map, dfl))
+    (main, map)
 
   let map2 (f : form -> form -> form) (poe1 : exnpost) (poe2 : exnpost) =
     let main, exnmap =
@@ -614,34 +613,28 @@ module POE = struct
 
   let exists (f : form -> bool) (poe : exnpost) =
       f poe.main
-    || Mp.exists (fun _ -> f) (fst poe.exnmap)
-    || omap_dfl f false (snd poe.exnmap)
+    || Mp.exists (fun _ -> f) poe.exnmap
 
   let forall (f : form -> bool) (poe : exnpost) =
       f poe.main
-    && Mp.for_all (fun _ -> f) (fst poe.exnmap)
-    && omap_dfl f true (snd poe.exnmap)
+    && Mp.for_all (fun _ -> f) poe.exnmap
 
   let forall2 (f : form -> form -> bool) (poe1 : exnpost) (poe2 : exnpost) =
       f poe1.main poe2.main
-    && Mp.equal f (fst poe1.exnmap) (fst poe2.exnmap)
-    && oeq f (snd poe1.exnmap) (snd poe2.exnmap)
+    && Mp.equal f poe1.exnmap poe2.exnmap
 
-  let to_list_pre ((main, (map, d)) : 'a prepoe) =
-    let l =
-      Mp.fold
-        (fun _ p1 a -> p1 :: a)
-        map
-        [main]
-    in otolist d @ l
+  let to_list_pre ((main, map) : 'a prepoe) =
+    Mp.fold
+      (fun _ p1 a -> p1 :: a)
+      map
+      [main]
 
   let to_list (poe : exnpost) =
     to_list_pre (destruct poe)
 
   let fold (tx : 'a -> form -> 'a) (state : 'a) (poe : exnpost)  =
     let state = tx state poe.main in
-    let state = Mp.fold (fun _ f state -> tx state f) (fst poe.exnmap) state in
-    let state = ofold (fun f state -> tx state f) state (snd poe.exnmap) in
+    let state = Mp.fold (fun _ f state -> tx state f) poe.exnmap state in
     state
 
   let iter (tx : form -> unit) (poe : exnpost)  =
@@ -657,13 +650,7 @@ module POE = struct
     f poe1.main poe2.main;
     Mp.iter
       (fun _ (a, b) -> f a b)
-      (Mp.merge (fun _ -> merge) (fst poe1.exnmap) (fst poe2.exnmap));
-    begin
-      match snd poe1.exnmap, snd poe2.exnmap with
-      | None, None -> ()
-      | Some a, Some b -> f a b
-      | _, _ -> assert false
-    end
+      (Mp.merge (fun _ -> merge) poe1.exnmap poe2.exnmap)
 end
 
 (* ----------------------------------------------------------------- *)
@@ -1059,8 +1046,7 @@ let b_hash (bs : bindings) =
 (*-------------------------------------------------------------------- *)
 let posts_equal (poe1 : exnpost) (poe2 : exnpost) =
      f_equal poe1.main poe2.main
-  && Mp.equal f_equal (fst poe1.exnmap) (fst poe2.exnmap)
-  && oeq f_equal (snd poe1.exnmap) (snd poe2.exnmap)
+  && Mp.equal f_equal poe1.exnmap poe2.exnmap
 
 (*-------------------------------------------------------------------- *)
 let hf_equal hf1 hf2 =
@@ -1141,13 +1127,9 @@ let post_hash (p : path) (f : form) =
   Why3.Hashcons.combine (EcPath.p_hash p) (f_hash f)
 
 let posts_hash (poe : exnpost) =
-  let h =
-    Why3.Hashcons.combine
-      (f_hash poe.main) (omap_dfl f_hash 0 (snd poe.exnmap))
-  in
-    Mp.fold
-      (fun e f a -> Why3.Hashcons.combine a (post_hash e f))
-      (fst poe.exnmap) h
+  Mp.fold
+    (fun e f a -> Why3.Hashcons.combine a (post_hash e f))
+    poe.exnmap (f_hash poe.main)
 
 (* -------------------------------------------------------------------- *)
 let hf_hash hf =
@@ -1510,10 +1492,9 @@ module Hsform = Why3.Hashcons.Make (struct
 
   let posts_fv (poe : exnpost) =
     let fv = f_fv poe.main in
-    let fv = snd poe.exnmap |> omap f_fv |> odfl fv in
     Mp.fold
       (fun _ f acc -> fv_union (f_fv f) acc)
-      (fst poe.exnmap) fv
+      poe.exnmap fv
 
   let fv_node f =
     let union ex nodes =
diff --git a/src/ecAst.mli b/src/ecAst.mli
index 13aabe0faa..c308a0a534 100644
--- a/src/ecAst.mli
+++ b/src/ecAst.mli
@@ -300,7 +300,7 @@ and bdHoareS = {
 
 and exnpost = {
   main   : form;
-  exnmap : form Mp.t * form option;
+  exnmap : form Mp.t;
 }
 
 and ss_inv = {
@@ -370,7 +370,7 @@ type hs_inv = {
 }
 
 (* -------------------------------------------------------------------- *)
-type 'a prepoe = 'a * ('a Mp.t * 'a option)
+type 'a prepoe = 'a * ('a Mp.t)
 
 module POE : sig
   val empty : form -> exnpost
@@ -381,9 +381,9 @@ module POE : sig
 
   val lower : hs_inv -> ss_inv
 
-  val mk : form -> (form Mp.t * form option) -> exnpost
+  val mk : form -> form Mp.t -> exnpost
 
-  val destruct : exnpost -> form * (form Mp.t * form option)
+  val destruct : exnpost -> form * (form Mp.t)
 
   val to_list_pre : 'a prepoe -> 'a list
 
diff --git a/src/ecCoreLib.ml b/src/ecCoreLib.ml
index 777ac5ad32..75a116bf10 100644
--- a/src/ecCoreLib.ml
+++ b/src/ecCoreLib.ml
@@ -10,6 +10,9 @@ let i_top  = "Top"
 let i_self = "Self"
 let p_top  = EcPath.psymbol i_top
 
+let i_wild = "_"
+let p_wild = EcPath.psymbol i_wild
+
 (* -------------------------------------------------------------------- *)
 let i_Pervasive = "Pervasive"
 let p_Pervasive = EcPath.pqname p_top i_Pervasive
diff --git a/src/ecCoreLib.mli b/src/ecCoreLib.mli
index 53892b4a70..cb3388b969 100644
--- a/src/ecCoreLib.mli
+++ b/src/ecCoreLib.mli
@@ -23,6 +23,9 @@ val i_top  : symbol
 val i_self : symbol
 val p_top  : path
 
+val i_wild : symbol
+val p_wild : path
+
 (* -------------------------------------------------------------------- *)
 val i_Pervasive : symbol
 val p_Pervasive : path
diff --git a/src/ecPrinting.ml b/src/ecPrinting.ml
index c3f29cdfac..3eede8fb75 100644
--- a/src/ecPrinting.ml
+++ b/src/ecPrinting.ml
@@ -1973,7 +1973,12 @@ and pp_form_core_r
       let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
       let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
       let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
-      let { main = post; exnmap = (poe, d) } = (hf_po hf).hsi_inv in
+      let { main = post; exnmap = poe } = (hf_po hf).hsi_inv in
+      let poe, d =
+        match EcPath.Mp.find EcCoreLib.p_wild poe with
+        | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+        | exception Not_found -> poe, None
+      in
       Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
         (pp_funname ppe) hf.hf_f
         (pp_pl_mem_binding pm ppe) hf.hf_m
@@ -1983,7 +1988,12 @@ and pp_form_core_r
 
   | FhoareS hs ->
       let ppe = PPEnv.push_mem ppe ~active:true hs.hs_m in
-      let { main = post; exnmap = (poe, d); } = (hs_po hs).hsi_inv in
+      let { main = post; exnmap = poe; } = (hs_po hs).hsi_inv in
+      let poe, d =
+        match EcPath.Mp.find EcCoreLib.p_wild poe with
+        | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+        | exception Not_found -> poe, None
+      in
       let pm = debug_mode || (fst hs.hs_m).id_symb <> "&hr" in
       Format.fprintf fmt "hoare[@[<hov 2>@ %a %a:@ @[%a ==>@ %a@ %a]@]]"
         (pp_stmt_for_form ppe) hs.hs_s
@@ -3079,7 +3089,12 @@ let pp_hoareF (ppe : PPEnv.t) ?prpo fmt hf =
   let ppepr = PPEnv.create_and_push_mem ppe ~active:true mepr in
   let ppepo = PPEnv.create_and_push_mem ppe ~active:true mepo in
 
-  let { main = post; exnmap = (poe, d); } = (hf_po hf).hsi_inv in
+  let { main = post; exnmap = poe; } = (hf_po hf).hsi_inv in
+  let poe, d =
+    match EcPath.Mp.find EcCoreLib.p_wild poe with
+    | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+    | exception Not_found -> poe, None
+  in
 
   Format.fprintf fmt "%a@\n%!" (pp_pre ppepr ?prpo) (hf_pr hf).inv;
   let pm = debug_mode || hf.hf_m.id_symb <> "&hr" in
@@ -3093,7 +3108,12 @@ let pp_hoareS (ppe : PPEnv.t) ?prpo fmt hs =
   let ppef = PPEnv.push_mem ppe ~active:true hs.hs_m in
   let ppnode = collect2_s ppef hs.hs_s.s_node [] in
 
-  let { main = post; exnmap = (poe, d); } = (hs_po hs).hsi_inv in
+  let { main = post; exnmap = poe; } = (hs_po hs).hsi_inv in
+  let poe, d =
+    match EcPath.Mp.find EcCoreLib.p_wild poe with
+    | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+    | exception Not_found -> poe, None
+  in
 
   let ppnode = c_ppnode ~width:ppe.PPEnv.ppe_width ppef ppnode in
 
diff --git a/src/ecProofTyping.ml b/src/ecProofTyping.ml
index d59d56d6dd..faa6e0acf4 100644
--- a/src/ecProofTyping.ml
+++ b/src/ecProofTyping.ml
@@ -89,9 +89,9 @@ let pf_process_pattern pe hyps fp =
 let pf_process_poe hyps poe =
   let env  = LDecl.toenv hyps in
   let ue = unienv_of_hyps hyps in
-  let m, d = EcTyping.trans_poe env ue poe in
+  let m = EcTyping.trans_poe env ue poe in
   let ts  = Tuni.subst (EcUnify.UniEnv.close ue) in
-  Mp.map (EcFol.Fsubst.f_subst ts) m, omap (EcFol.Fsubst.f_subst ts) d
+  Mp.map (EcFol.Fsubst.f_subst ts) m
 
 (* ------------------------------------------------------------------ *)
 let tc1_process_form_opt ?mv tc oty pf =
@@ -262,7 +262,14 @@ let destruct_exists ?(reduce = true) hyps fp : dexists option =
     lazy_destruct ~reduce hyps doit fp
 
 (* -------------------------------------------------------------------- *)
-let merge2_poe_list (poe1,d1) (poe2,d2) =
+let merge2_poe_list poe1 poe2 =
+  let aux poe =
+    match EcPath.Mp.find EcCoreLib.p_wild poe with
+    | x -> EcPath.Mp.remove EcCoreLib.p_wild poe, Some x
+    | exception Not_found -> poe, None
+  in
+  let poe1, d1 = aux poe1 in
+  let poe2, d2 = aux poe2 in
   let get_default d =
     match d with
     | Some d -> d
diff --git a/src/ecProofTyping.mli b/src/ecProofTyping.mli
index 20bef62cbb..21c5411621 100644
--- a/src/ecProofTyping.mli
+++ b/src/ecProofTyping.mli
@@ -33,7 +33,7 @@ val pf_process_xreal    : proofenv -> ?mv:metavs -> LDecl.hyps -> pformula -> fo
 
 val pf_process_exp      : proofenv -> LDecl.hyps -> [`InProc|`InOp] -> ty option -> pexpr -> expr
 val pf_process_pattern  : proofenv -> LDecl.hyps -> pformula -> ptnenv * form
-val pf_process_poe      : LDecl.hyps -> phoare_exception -> form Mp.t * form option
+val pf_process_poe      : LDecl.hyps -> phoare_exception -> form Mp.t
 
 (* Typing in the [proofenv] implies for the [tcenv].
  * Typing exceptions are recasted in the proof env. context *)
@@ -83,7 +83,4 @@ val destruct_product: ?reduce:bool -> EcEnv.LDecl.hyps -> form -> dproduct optio
 val destruct_exists : ?reduce:bool -> EcEnv.LDecl.hyps -> form -> dexists  option
 
 (* -------------------------------------------------------------------- *)
-val merge2_poe_list :
-  form Mp.t * form option ->
-  form Mp.t * form option ->
-  form list
+val merge2_poe_list : form Mp.t -> form Mp.t  -> form list
diff --git a/src/ecReduction.ml b/src/ecReduction.ml
index 261740e899..8a9efdbebf 100644
--- a/src/ecReduction.ml
+++ b/src/ecReduction.ml
@@ -1344,19 +1344,13 @@ let ztuple args1 args2 ty stk = zpush Ztuple [] args1 args2 ty stk
 let zproj i ty stk = zpush (Zproj i) [] [] [] ty stk
 let zhl f fs1 fs2 stk = zpush (Zhl f) [] fs1 fs2 f.f_ty stk
 
-let zpoe ({ exnmap = (epost, d) } : exnpost) (dpoe : form list) =
-  let d, dpoe =
-    match d, dpoe with
-    | None, _ -> None, dpoe
-    | _, h::q -> Some h, q
-    | _, _ -> assert false
-  in
+let zpoe ({ exnmap = epost } : exnpost) (dpoe : form list) =
   let key = List.map fst (Mp.bindings epost) in
   let poe =
     List.fold_left2
       (fun m a b -> Mp.add a b m)
       Mp.empty key dpoe
-  in (poe,d)
+  in poe
 
 let zpop ri side f hd =
   let args =
@@ -1376,16 +1370,16 @@ let zpop ri side f hd =
   | Zproj i, [f1]      -> f_proj f1 i hd.se_ty
   | Zhl {f_node = FhoareF hf}, (pr :: po :: dpoe) ->
     let m = hf.hf_m in
-    let poe, d = zpoe (hf_po hf).hsi_inv dpoe in
-    f_hoareF {m;inv=pr} hf.hf_f { hsi_m = m; hsi_inv = POE.mk po (poe, d); }
+    let poe = zpoe (hf_po hf).hsi_inv dpoe in
+    f_hoareF {m;inv=pr} hf.hf_f { hsi_m = m; hsi_inv = POE.mk po poe; }
   | Zhl {f_node = FhoareS hs}, (pr :: po :: dpoe) ->
     let m = fst hs.hs_m in
-    let (poe, d) = zpoe (hs_po hs).hsi_inv dpoe in
+    let poe = zpoe (hs_po hs).hsi_inv dpoe in
     f_hoareS
       (snd hs.hs_m)
       { m; inv = pr}
       hs.hs_s
-      { hsi_m = m ; hsi_inv = POE.mk po (poe, d); }
+      { hsi_m = m ; hsi_inv = POE.mk po poe; }
   | Zhl {f_node = FeHoareF hf}, [pr;po] ->
     let m = hf.ehf_m in
     f_eHoareF {m;inv=pr} hf.ehf_f {m;inv=po}
@@ -1510,9 +1504,9 @@ let rec conv ri env f1 f2 stk =
     ->
       let pr2 = (ss_inv_rebind (hf_pr hf2) hf1.hf_m).inv in
       let po2 = (hs_inv_rebind (hf_po hf2) hf1.hf_m).hsi_inv in
-      let aux { main = post; exnmap = (poe, d); } =
+      let aux { main = post; exnmap = poe; } =
         let poe = List.map snd (Mp.bindings poe) in
-        match d with None -> post :: poe | Some d -> post :: d :: poe
+        post :: poe
       in
       let lf1 = aux (hf_po hf1).hsi_inv in
       let lf2 = aux po2 in
@@ -1524,9 +1518,9 @@ let rec conv ri env f1 f2 stk =
     | _subst ->
       let pr2 = (ss_inv_rebind (hs_pr hs2) (fst hs1.hs_m)).inv in
       let po2 = (hs_inv_rebind (hs_po hs2) (fst hs1.hs_m)).hsi_inv in
-      let aux { main = post; exnmap = (poe, d) } =
+      let aux { main = post; exnmap = poe } =
         let poe = List.map snd (Mp.bindings poe) in
-        match d with None -> post :: poe | Some d -> post :: d :: poe
+        post :: poe
       in
       let lf1 = aux (hs_po hs1).hsi_inv in
       let lf2 = aux po2 in
diff --git a/src/ecSubst.ml b/src/ecSubst.ml
index bc52ff4ba4..6ffac9215e 100644
--- a/src/ecSubst.ml
+++ b/src/ecSubst.ml
@@ -811,14 +811,13 @@ and subst_module (s : subst) (m : module_expr) =
 and subst_hs_inv (s : subst) (inv : hs_inv) =
   let s = add_memory s inv.hsi_m inv.hsi_m in
   let main = subst_form s inv.hsi_inv.main in
-  let map =
+  let exnmap =
     Mp.fold (fun p f m ->
       let p = subst_path s p in
       let f = subst_form s f in
       Mp.add p f m
-    ) (fst inv.hsi_inv.exnmap) Mp.empty in
-  let dfl = omap (subst_form s) (snd inv.hsi_inv.exnmap) in
-  { hsi_inv = { main; exnmap = (map, dfl) }; hsi_m = inv.hsi_m }
+    ) inv.hsi_inv.exnmap Mp.empty in
+  { hsi_inv = { main; exnmap }; hsi_m = inv.hsi_m }
 
 (* -------------------------------------------------------------------- *)
 let subst_modsig ?params (s : subst) (comps : module_sig) =
diff --git a/src/ecTyping.ml b/src/ecTyping.ml
index 266b86dc87..d23b8dbabc 100644
--- a/src/ecTyping.ml
+++ b/src/ecTyping.ml
@@ -1444,12 +1444,13 @@ let trans_match_exn ~loc env ue pbs =
   let rec fill_branches tbl pbs =
     match pbs with
     | [] ->
-      tbl, None
+      tbl
 
     | (None, body) :: pbs ->
       if pbs <> [] then
         tyerror loc env (InvalidMatch FXE_MatchDupBranches);
-      tbl, Some body
+
+      Mp.add EcCoreLib.p_wild ([], body) tbl
 
     | (Some (x, bds), body) :: pbs ->
       if Mp.mem x tbl then
@@ -3540,8 +3541,8 @@ and trans_form_or_pattern env mode ?mv ?ps ue pf tt =
         unify_or_fail qenv ue post.pnormal.pl_loc ~expct:tbool post'.f_ty;
 
         let penv_e = EcEnv.Fun.inv_memenv1 m env in
-        let epost', dpost' = trans_poe penv_e ue post.pexcept in
-        f_hoareF {m;inv=pre'} fpath { hsi_m = m; hsi_inv = POE.mk post' (epost', dpost'); }
+        let epost' = trans_poe penv_e ue post.pexcept in
+        f_hoareF {m;inv=pre'} fpath { hsi_m = m; hsi_inv = POE.mk post' epost'; }
 
     | PFehoareF (m, pre, gp, post) ->
         if mode <> `Form then
@@ -3687,15 +3688,13 @@ and trans_prop env ?mv ue pf =
 and trans_poe penv_e ue poe =
   let loc = poe.pl_loc in
   let poe = poe.pl_desc in
-  let branches, dfl = trans_match_exn ~loc penv_e ue poe in
-  let epost = Mp.map (fun (lcs, body) ->
-     let env = EcEnv.Var.bind_locals lcs penv_e in
-     let bdy  = trans_prop env ue body in
-     f_lambda (List.map (snd_map gtty) lcs) bdy) branches in
-   let dpost = omap (fun body ->
-     let bdy = trans_prop penv_e ue body in
-     bdy) dfl in
-   epost, dpost
+  let branches = trans_match_exn ~loc penv_e ue poe in
+  Mp.map
+    (fun (lcs, body) ->
+       let env = EcEnv.Var.bind_locals lcs penv_e in
+       let bdy  = trans_prop env ue body in
+       f_lambda (List.map (snd_map gtty) lcs) bdy)
+    branches
 
 (* -------------------------------------------------------------------- *)
 and trans_pattern env ps ue pf =
diff --git a/src/ecTyping.mli b/src/ecTyping.mli
index 6722b92b3e..01dce716e9 100644
--- a/src/ecTyping.mli
+++ b/src/ecTyping.mli
@@ -266,7 +266,7 @@ val trans_poe :
   EcEnv.env ->
   EcUnify.unienv ->
   EcParsetree.phoare_exception ->
-  EcFol.form EcPath.Mp.t * EcFol.form option
+  EcFol.form EcPath.Mp.t
 
 (* -------------------------------------------------------------------- *)
 val trans_memtype :
diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml
index 87a3bc727e..95b772dce8 100644
--- a/src/phl/ecPhlCall.ml
+++ b/src/phl/ecPhlCall.ml
@@ -71,10 +71,10 @@ let t_hoare_call fpre fpost tc =
   (* substitute memories *)
   let fpre = (ss_inv_rebind fpre m) in
   let fpost = hs_inv_rebind fpost m in
-  let { main = inv; exnmap = (fepost, fd); } = fpost.hsi_inv in
+  let inv,fepost = POE.destruct fpost.hsi_inv in
   let fpost = {m;inv} in
   (* The wp *)
-  let { main = post; exnmap = (epost, d); } = (hs_po hs).hsi_inv in
+  let post, epost = POE.destruct (hs_po hs).hsi_inv in
   let pvres = pv_res in
   let vres = EcIdent.create "result" in
   let fres = {m;inv=f_local vres fsig.fs_ret} in
@@ -88,7 +88,7 @@ let t_hoare_call fpre fpost tc =
   let spre = subst_args_call env m (e_tuple args) PVM.empty in
   let post = map_ss_inv2 f_anda_simpl (map_ss_inv1 (PVM.subst env spre) fpre) post in
 
-  let poe = TTC.merge2_poe_list (epost,d) (fepost,fd) in
+  let poe = TTC.merge2_poe_list epost fepost in
   let poe = List.map (fun inv -> {m;inv}) poe in
   let penv_e = EcEnv.Fun.inv_memenv1 m env in
   let poe = List.map (generalize_mod_ss_inv penv_e modi) poe in
@@ -96,7 +96,7 @@ let t_hoare_call fpre fpost tc =
   let post = List.fold (map_ss_inv2 f_anda_simpl) post poe in
   let post = {
     hsi_m   = post.m;
-    hsi_inv = { main = post.inv; exnmap = (epost, d); };
+    hsi_inv = { main = post.inv; exnmap = epost };
   } in
   let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in
   FApi.xmutate1 tc `HlCall [f_concl; concl]
@@ -484,8 +484,8 @@ let process_call side info tc =
       let pre  = TTC.pf_process_form !!tc penv tbool pre  in
       let post = TTC.pf_process_form !!tc qenv tbool post in
       let env_e = LDecl.inv_memenv1 m hyps in
-      let (poe, d) = TTC.pf_process_poe env_e poe in
-      f_hoareF {m; inv = pre} f { hsi_m = m; hsi_inv = { main = post; exnmap = (poe, d); } }
+      let poe = TTC.pf_process_poe env_e poe in
+      f_hoareF {m; inv = pre} f { hsi_m = m; hsi_inv = { main = post; exnmap = poe; } }
 
     | _ -> tc_error !!tc "the conclusion is not a hoare" in
 
diff --git a/src/phl/ecPhlConseq.ml b/src/phl/ecPhlConseq.ml
index 8165d6904d..454800a191 100644
--- a/src/phl/ecPhlConseq.ml
+++ b/src/phl/ecPhlConseq.ml
@@ -64,18 +64,18 @@ let t_hoareF_conseq pre post tc =
   let hf  = tc1_as_hoareF tc in
   let pre = ss_inv_rebind pre hf.hf_m in
   let post = hs_inv_rebind post hf.hf_m in
-  let { main = post; exnmap = (epost, d); } = post.hsi_inv in
-  let { main = fpost; exnmap = (fepost, fd); } = (hf_po hf).hsi_inv in
+  let post, epost = POE.destruct post.hsi_inv in
+  let fpost, fepost = POE.destruct (hf_po hf).hsi_inv in
   let mpr,mpo = EcEnv.Fun.hoareF_memenv hf.hf_m hf.hf_f env in
   let m = hf.hf_m in
   let cond1, cond2 =
     conseq_cond_ss (hf_pr hf) {m;inv=fpost} pre {m;inv=post}
   in
-  let cond2e = TTC.merge2_poe_list (fepost,fd) (epost,d) in
+  let cond2e = TTC.merge2_poe_list fepost epost in
   let cond2 = List.fold f_and cond2.inv cond2e in
   let concl1 = f_forall_mems_ss_inv mpr cond1 in
   let concl2 = f_forall_mems_ss_inv mpo {m;inv=cond2} in
-  let concl3 = f_hoareF pre hf.hf_f { hsi_m = m; hsi_inv = POE.mk post (epost, d)} in
+  let concl3 = f_hoareF pre hf.hf_f { hsi_m = m; hsi_inv = POE.mk post epost} in
   FApi.xmutate1 tc `Conseq [concl1; concl2; concl3]
 
 (* -------------------------------------------------------------------- *)
@@ -84,18 +84,18 @@ let t_hoareS_conseq pre post tc =
   let hs = tc1_as_hoareS tc in
   let pre = ss_inv_rebind pre (fst hs.hs_m) in
   let post = hs_inv_rebind post (fst hs.hs_m) in
-  let (post, (epost, d)) = POE.destruct post.hsi_inv in
-  let (fpost, (fepost,fd)) = POE.destruct (hs_po hs).hsi_inv in
+  let post, epost = POE.destruct post.hsi_inv in
+  let fpost, fepost = POE.destruct (hs_po hs).hsi_inv in
   let m = fst hs.hs_m in
   let cond1, cond2 =
     conseq_cond_ss (hs_pr hs) {m;inv=fpost} pre {m;inv=post}
   in
-  let cond2e = TTC.merge2_poe_list (fepost,fd) (epost,d) in
+  let cond2e = TTC.merge2_poe_list fepost epost in
   let cond2 = List.fold f_and cond2.inv cond2e in
   let concl1 = f_forall_mems_ss_inv hs.hs_m cond1 in
   let concl2 = f_forall_mems_ss_inv hs.hs_m {m=fst hs.hs_m;inv=cond2} in
   let concl3 =
-    f_hoareS (snd hs.hs_m) pre hs.hs_s { hsi_m = m; hsi_inv = POE.mk post (epost, d); }
+    f_hoareS (snd hs.hs_m) pre hs.hs_s { hsi_m = m; hsi_inv = POE.mk post epost }
   in
   FApi.xmutate1 tc `HlConseq [concl1; concl2; concl3]
 
@@ -224,14 +224,14 @@ let t_equivS_conseq pre post tc =
 let t_conseq pre post tc =
   match (FApi.tc1_goal tc).f_node, pre, post with
   | FhoareF hf, Inv_ss pre, Inv_ss post ->
-    let (epost, d) = (hf_po hf).hsi_inv.exnmap in
+    let epost = (hf_po hf).hsi_inv.exnmap in
     let post = ss_inv_rebind post (hf_po hf).hsi_m in
-    let post = { hsi_m = (hf_po hf).hsi_m; hsi_inv = POE.mk post.inv (epost, d)} in
+    let post = { hsi_m = (hf_po hf).hsi_m; hsi_inv = POE.mk post.inv epost} in
     t_hoareF_conseq pre post tc
   | FhoareS hs, Inv_ss pre, Inv_ss post ->
-    let (epost, d) = (hs_po hs).hsi_inv.exnmap in
+    let epost = (hs_po hs).hsi_inv.exnmap in
     let post = ss_inv_rebind post (hs_po hs).hsi_m in
-    let post = { hsi_m = (hs_po hs).hsi_m; hsi_inv = POE.mk post.inv (epost, d); } in
+    let post = { hsi_m = (hs_po hs).hsi_m; hsi_inv = POE.mk post.inv epost } in
     t_hoareS_conseq pre post tc
   | FhoareF _, Inv_ss pre, Inv_hs post ->
     t_hoareF_conseq pre post tc
@@ -349,10 +349,10 @@ let cond_hoareF_notmod ?(mk_other=false) tc (cond: ss_inv) =
 let t_hoareF_notmod post tc =
   let hf = tc1_as_hoareF tc in
   let p = hs_inv_rebind post hf.hf_m in
-  let (post, (epost, d)) = POE.destruct p.hsi_inv in
-  let (fpost, (fepost, fd)) = POE.destruct (hf_po hf).hsi_inv in
+  let post, epost = POE.destruct p.hsi_inv in
+  let fpost, fepost = POE.destruct (hf_po hf).hsi_inv in
   let cond = f_imp post fpost in
-  let econd1 = TTC.merge2_poe_list (fepost,fd) (epost,d) in
+  let econd1 = TTC.merge2_poe_list fepost epost in
   let cond1 = List.fold f_and cond econd1 in
   let cond1, _, _ = cond_hoareF_notmod tc {m=hf.hf_m;inv=cond1} in
   let cond2 = f_hoareF (hf_pr hf) hf.hf_f p in
@@ -377,10 +377,10 @@ let cond_hoareS_notmod ?(mk_other=false) tc cond =
 let t_hoareS_notmod post tc =
   let hs = tc1_as_hoareS tc in
   let p = hs_inv_rebind post (fst hs.hs_m) in
-  let (post, (epost, d)) = POE.destruct p.hsi_inv in
-  let (fpost, (fepost, fd)) = POE.destruct (hs_po hs).hsi_inv in
+  let post, epost = POE.destruct p.hsi_inv in
+  let fpost, fepost = POE.destruct (hs_po hs).hsi_inv in
   let cond = f_imp post fpost in
-  let econd1 = TTC.merge2_poe_list (fepost,fd) (epost,d) in
+  let econd1 = TTC.merge2_poe_list fepost epost in
   let cond1 = List.fold f_and cond econd1 in
   let cond1, _, _ = cond_hoareS_notmod tc {m=fst hs.hs_m;inv=cond1} in
   let cond2 = f_hoareS (snd hs.hs_m) (hs_pr hs) hs.hs_s p in
@@ -1707,12 +1707,12 @@ let process_conseq_1 notmod ((info1, info2, info3) : conseq_ppterm option tuple3
     let (pre, post, bd) = match gpre, gpost with
       | Inv_ss gpre, Inv_hs gpost ->
         let bd = bd |> omap (process_info !!tc penv gpre.m) in
-        let (gp, (gpoe, gd)) = POE.destruct gpost.hsi_inv in
+        let gp, gpoe = POE.destruct gpost.hsi_inv in
         let post = post |> odfl gp in
-        let (poe,d) = poe |> odfl (gpoe, gd) in
+        let poe = poe |> odfl gpoe in
         (
           Inv_ss { inv = pre; m = gpre.m; },
-          Inv_hs { hsi_inv = POE.mk post (poe, d); hsi_m = gpost.hsi_m },
+          Inv_hs { hsi_inv = POE.mk post poe; hsi_m = gpost.hsi_m },
           bd
         )
       | _ -> tc_error !!tc "conseq: pre and post must be of the same kind"
@@ -1763,12 +1763,12 @@ let process_conseq_1 notmod ((info1, info2, info3) : conseq_ppterm option tuple3
     let (pre, post, bd) = match gpre, gpost with
       | Inv_ss gpre, Inv_hs gpost ->
         let bd = bd |> omap (process_info !!tc penv gpre.m) in
-        let (gp, (gpoe, gd)) = POE.destruct gpost.hsi_inv in
+        let gp, gpoe = POE.destruct gpost.hsi_inv in
         let post = post |> odfl gp in
-        let (poe, d) = poe |> odfl (gpoe, gd) in
+        let poe = poe |> odfl gpoe in
         (
           Inv_ss { inv = pre; m = gpre.m; },
-          Inv_hs { hsi_inv = POE.mk post (poe, d); hsi_m = gpost.hsi_m; },
+          Inv_hs { hsi_inv = POE.mk post poe; hsi_m = gpost.hsi_m; },
           bd
         )
       | _ -> tc_error !!tc "conseq: pre and post must be of the same kind"
diff --git a/src/phl/ecPhlFun.ml b/src/phl/ecPhlFun.ml
index 17471d07f1..ebee1e8fea 100644
--- a/src/phl/ecPhlFun.ml
+++ b/src/phl/ecPhlFun.ml
@@ -79,11 +79,11 @@ let t_hoareF_fun_def_r tc =
   let (memenv, (fsig, fdef), env) = Fun.hoareS hf.hf_m f env in
   let m = EcMemory.memory memenv in
   let fres = odfl {m;inv=f_tt} (omap (ss_inv_of_expr m) fdef.f_ret) in
-  let (post, (epost, d)) = POE.destruct (hf_po hf).hsi_inv in
+  let post, epost = POE.destruct (hf_po hf).hsi_inv in
   let post = {m=(hf_po hf).hsi_m;inv=post} in
   let post = map_ss_inv2 (PVM.subst1 env pv_res m) fres  post in
   let pre  = map_ss_inv1 (PVM.subst env (subst_pre env fsig m PVM.empty)) (hf_pr hf) in
-  let post = { hsi_m = post.m; hsi_inv = POE.mk post.inv (epost, d); } in
+  let post = { hsi_m = post.m; hsi_inv = POE.mk post.inv epost; } in
   let concl' = f_hoareS (snd memenv) pre fdef.f_body post in
   FApi.xmutate1 tc `FunDef [concl']
 
diff --git a/src/phl/ecPhlWp.ml b/src/phl/ecPhlWp.ml
index 535d936210..c29dd8b0d2 100644
--- a/src/phl/ecPhlWp.ml
+++ b/src/phl/ecPhlWp.ml
@@ -12,7 +12,7 @@ open EcLowPhlGoal
 module LowInternal = struct
   exception No_wp
 
-  let find_poe hyps memenv (epost,d) (e:EcTypes.expr) =
+  let find_poe hyps memenv epost (e:EcTypes.expr) =
     let m = EcMemory.memory memenv in
     let f = form_of_expr ~m e in
     let f = EcReduction.h_red_until EcReduction.full_red hyps f in
@@ -20,9 +20,10 @@ module LowInternal = struct
     match Mp.find ex epost with
     | f -> f_app_simpl f args EcTypes.tbool
     | exception Not_found ->
-      match d with
-      | Some d -> d
-      | None -> tacuerror "missing postcondition for exception %a" EcPrinting.pp_path ex
+      match Mp.find EcCoreLib.p_wild epost with
+      | d -> d
+      | exception Not_found ->
+        tacuerror "missing postcondition for exception %a" EcPrinting.pp_path ex
 
 
   let wp_asgn_aux c_pre memenv lv e (lets, f) =
@@ -143,10 +144,10 @@ let wp
    (s        : stmt)
    (poe      : exnpost)
 =
-  let { main = post; exnmap = (epost, d) } = poe in
+  let post, epost = POE.destruct poe in
   let (r, letsf) =
     LowInternal.wp_stmt ?mc
-      onesided c_pre hyps m (List.rev s.s_node) ([], post) (epost,d)
+      onesided c_pre hyps m (List.rev s.s_node) ([], post) epost
   in
   let pre = mk_let_of_lv_substs ?mc ~uselet (EcEnv.LDecl.toenv hyps) letsf in
   (List.rev r, pre)
@@ -168,12 +169,12 @@ module TacInternal = struct
     let hs = tc1_as_hoareS tc in
     let (s_hd, s_wp) = o_split env i hs.hs_s in
     let s_wp = EcModules.stmt s_wp in
-    let { exnmap = (eposts, d) } as post = (hs_po hs).hsi_inv in
+    let { exnmap = eposts } as post = (hs_po hs).hsi_inv in
     let s_wp, post = wp ~uselet ~onesided:true hyps hs.hs_m s_wp post in
     check_wp_progress tc i hs.hs_s s_wp;
     let s = EcModules.stmt (s_hd @ s_wp) in
     let m = fst hs.hs_m in
-    let post = { hsi_m = m; hsi_inv = { main = post; exnmap = (eposts, d)}; } in
+    let post = { hsi_m = m; hsi_inv = { main = post; exnmap = eposts} } in
     let concl = f_hoareS (snd hs.hs_m) (hs_pr hs) s post in
     FApi.xmutate1 tc `Wp [concl]