diff --git a/src/kernel_services/ast_printing/description.ml b/src/kernel_services/ast_printing/description.ml
index df0de122d9ac9582d9de2752500c68a022d37055..e314dca611ad44aa5f4d27d8db5e9e31311bed5c 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 _ -> []