From c7ae51141120e8ad263dea4e4fa7ce75210b584e Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 7 Mar 2019 18:24:25 +0100
Subject: [PATCH] [printing] distinguish between check and assert when grouping
annotations
---
src/kernel_services/ast_printing/description.ml | 8 +++++---
1 file changed, 5 insertions(+), 3 deletions(-)
diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index df0de122d9a..e314dca611a 100644
--- a/src/kernel_services/ast_printing/description.ml
+++ b/src/kernel_services/ast_printing/description.ml
@@ -466,11 +466,13 @@ let for_order k = function
| [] -> [I k]
| bs -> I (succ k) :: named_order bs
let annot_order = function
- | {annot_content=AAssert(bs,_kind,np)} ->
+ | {annot_content=AAssert(bs,Check,np)} ->
for_order 0 bs @ named_order np.pred_name
- | {annot_content=AInvariant(bs,_,np)} ->
+ | {annot_content=AAssert(bs,Assert,np)} ->
for_order 2 bs @ named_order np.pred_name
- | _ -> [I 4]
+ | {annot_content=AInvariant(bs,_,np)} ->
+ for_order 4 bs @ named_order np.pred_name
+ | _ -> [I 6]
let loop_order = function
| Id_contract (active,b) -> [B b; A active]
| Id_loop _ -> []
--
GitLab