Commit 2142447e authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

WhyML: marks are ghost

parent dcd88e36
...@@ -66,11 +66,11 @@ let th_mark_old = ...@@ -66,11 +66,11 @@ let th_mark_old =
let fs_now = create_lsymbol (id_fresh "%now") [] (Some ty_mark) let fs_now = create_lsymbol (id_fresh "%now") [] (Some ty_mark)
let t_now = fs_app fs_now [] ty_mark let t_now = fs_app fs_now [] ty_mark
let e_now = e_lapp fs_now [] (ity_pur ts_mark []) let e_now = e_ghost (e_lapp fs_now [] (ity_pur ts_mark []))
(* [vs_old] appears in the postconditions given to the core API, (* [vs_old] appears in the postconditions given to the core API,
which expects every vsymbol to be a pure part of a pvsymbol *) which expects every vsymbol to be a pure part of a pvsymbol *)
let pv_old = create_pvsymbol (id_fresh "%old") ity_mark let pv_old = create_pvsymbol ~ghost:true (id_fresh "%old") ity_mark
let vs_old = pv_old.pv_vs let vs_old = pv_old.pv_vs
let t_old = t_var vs_old let t_old = t_var vs_old
......
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