Commit dd78e722 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

WP: no substitution of logic terms, but let-in instead

parent b375b98c
......@@ -612,7 +612,10 @@ and wp_desc env e q xq = match e.e_node with
(* NOTE: if you replace this t_subst by t_let or anything else,
you must handle separately the case "let mark = 'now in ...",
which requires 'now to be substituted for mark in q *)
t_subst_single v (to_term t) q
if ty_equal v.vs_ty ty_mark then
t_subst_single v (to_term t) q
else
t_let_close_simp v (to_term t) q
| Evalue pv ->
let v, q = open_post q in
let t = wp_label e (t_var pv.pv_vs) in
......
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