diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml index 6f74f1dcde905233dcfc5a0bc4817c3e1a54d1db..51be9bba036ec3825f0fefb6b82f905379c9345a 100644 --- a/src/plugins/wp/Conditions.ml +++ b/src/plugins/wp/Conditions.ml @@ -1056,7 +1056,7 @@ struct | Some m -> m | None -> let m = Lang.sigma () in - F.Subst.add_map m s.def ; + F.Subst.add_fun m (fun e -> Tmap.find e s.def) ; s.cache <- Some m ; m let e_apply s e = F.e_subst (subst s) e