From 0052e04ed739f2a779de071716e48d21b990c275 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 10 Sep 2020 13:35:16 +0200
Subject: [PATCH] [wp] update to new WP API after rebase
---
src/plugins/wp/MemLoader.ml | 2 +-
src/plugins/wp/MemTyped.ml | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index c1bc3500eac..b1abfb6af8f 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -323,7 +323,7 @@ struct
let low = M.is_init_range sigma obj loc e_one in
let lemma = p_equiv high low in
{
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = name ^ "_low" ; l_types = 0 ;
l_forall = F.p_vars lemma ;
l_triggers = [] ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index e910305304a..3536f05e422 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -546,7 +546,7 @@ module BASE = WpContext.Generator(Varinfo)
let m_init = p_call p_cinits [m] in
let init_prop = p_forall [a] (p_imply m_init init_access) in
Definitions.define_lemma {
- l_assumed = true ;
+ l_kind = `Axiom ;
l_name = prefix ^ "_init" ; l_types = 0 ;
l_triggers = [] ; l_forall = [] ;
l_lemma = init_prop ;
--
GitLab