Skip to content
Snippets Groups Projects
Commit 0052e04e authored by Virgile Prevosto's avatar Virgile Prevosto
Browse files

[wp] update to new WP API after rebase

parent a85ed511
No related branches found
No related tags found
No related merge requests found
...@@ -323,7 +323,7 @@ struct ...@@ -323,7 +323,7 @@ struct
let low = M.is_init_range sigma obj loc e_one in let low = M.is_init_range sigma obj loc e_one in
let lemma = p_equiv high low in let lemma = p_equiv high low in
{ {
l_assumed = true ; l_kind = `Axiom ;
l_name = name ^ "_low" ; l_types = 0 ; l_name = name ^ "_low" ; l_types = 0 ;
l_forall = F.p_vars lemma ; l_forall = F.p_vars lemma ;
l_triggers = [] ; l_triggers = [] ;
......
...@@ -546,7 +546,7 @@ module BASE = WpContext.Generator(Varinfo) ...@@ -546,7 +546,7 @@ module BASE = WpContext.Generator(Varinfo)
let m_init = p_call p_cinits [m] in let m_init = p_call p_cinits [m] in
let init_prop = p_forall [a] (p_imply m_init init_access) in let init_prop = p_forall [a] (p_imply m_init init_access) in
Definitions.define_lemma { Definitions.define_lemma {
l_assumed = true ; l_kind = `Axiom ;
l_name = prefix ^ "_init" ; l_types = 0 ; l_name = prefix ^ "_init" ; l_types = 0 ;
l_triggers = [] ; l_forall = [] ; l_triggers = [] ; l_forall = [] ;
l_lemma = init_prop ; l_lemma = init_prop ;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment