From 628bfb5df35ea2d1ae15ec2c7d90db70a539c950 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 10 Sep 2020 09:07:02 +0200
Subject: [PATCH] [wp] fix check lemma category
---
src/plugins/wp/wpPropId.ml | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/wpPropId.ml b/src/plugins/wp/wpPropId.ml
index 6b9f147e04d..ec5d88cd371 100644
--- a/src/plugins/wp/wpPropId.ml
+++ b/src/plugins/wp/wpPropId.ml
@@ -500,9 +500,8 @@ let user_prop_names p =
| IPDecrease {id_ca=Some ca} -> "@decreases"::code_annot_names ca
| IPDecrease _ -> [ "@decreases" ]
| IPLemma {il_name = a; il_pred = l} ->
- let cat = if l.tp_only_check then "@check" else "@lemma" in
- let names = cat::a::(ident_names l.tp_statement.pred_name)
- in begin
+ let names = "@lemma"::a::pred_names l in
+ begin
match LogicUsage.section_of_lemma a with
| LogicUsage.Toplevel _ -> names
| LogicUsage.Axiomatic ax -> ax.LogicUsage.ax_name::names
--
GitLab