Skip to content
Snippets Groups Projects
Commit 628bfb5d authored by Loïc Correnson's avatar Loïc Correnson Committed by Virgile Prevosto
Browse files

[wp] fix check lemma category

parent 1ce69a31
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
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