Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit a3fd11c4 authored by Sylvain Dailler's avatar Sylvain Dailler

Using replace of Term.ml in tactics rewrite and replace.

parent 37d64c87
......@@ -159,8 +159,7 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
failwith "After substitution, terms are not exactly identical"))
(* Replace all occurences of f1 by f2 in t *)
let rec replace_in_term f1 f2 t =
t_map (fun t -> if t_equal t f1 then f2 else replace_in_term f1 f2 t) t
let replace_in_term = Term.t_replace
(* TODO be careful with label copy in t_map *)
let replace rev f1 f2 t =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment