[WP] Improve Conditions.subst doc and fixes usages

src/plugins/wp/Auto.ml

@@ -85,7 +85,11 @@ let t_range e a b ~upper ~lower ~range s =
   ]
 
 let t_replace ?(equal="equal") ~src ~tgt (pi : Tactical.process) s =
-  let s' = Conditions.subst (fun e -> if e == src then tgt else e) s in
+  let s' =
+    Conditions.subst
+      (fun e -> if e == src then tgt else raise Not_found)
+      s
+  in
   (equal , (fst s, p_equal src tgt)) :: (pi s')
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/Conditions.mli

@@ -134,6 +134,7 @@ val subst : (term -> term) -> sequent -> sequent
     Function [f] should only transform the head of the predicate, and can assume
     its sub-terms have been already substituted. The atomic substitution is also applied
     to predicates.
+    [f] should raise [Not_found] on terms that must not be replaced
 *)
 
 val introduction : sequent -> sequent option

src/plugins/wp/TacOverflow.ml

@@ -48,7 +48,7 @@ class overflow =
                 "In-Range", (hs , cond) ;
                 "No-Overflow" ,
                 Conditions.subst
-                  (fun u -> if u == e then v else u)
+                  (fun u -> if u == e then v else raise Not_found)
                   (hs , F.p_imply cond g)
               ])
       | _ -> Not_applicable

src/plugins/wp/Tactical.ml

@@ -366,7 +366,7 @@ let rewrite ?at patterns sequent =
     (fun (descr,guard,src,tgt) ->
        let sequent =
          Conditions.subst
-           (fun e -> if e == src then tgt else e)
+           (fun e -> if e == src then tgt else raise Not_found)
            sequent in
        let step = Conditions.(step ~descr (When guard)) in
        descr , Conditions.insert ?at step sequent