Introduce an attribute to unrefine type arguments

doc/old/tutorial/code/solutions/EtM.CPA.fst

@@ -37,6 +37,7 @@ let ivsize = blockSize AES_128_CBC
 let keysize = 16
 type aes_key = lbytes keysize (* = b:bytes{B.length b = keysize} *)
 type msg = plain
+[@@do_not_unrefine]
 type cipher = b:bytes{B.length b >= ivsize}
 (* MK: minimal cipher length twice blocksize? *)
 

examples/crypto/HyE.AE.fsti

@@ -32,6 +32,7 @@ let ivsize = aeadRealIVSize AES_128_GCM
 let keysize = aeadKeySize AES_128_GCM
 type aes_key = lbytes keysize (* = b:bytes{B.length b = keysize} *)
 type msg = Plain.t
+[@@do_not_unrefine]
 type cipher = b:bytes{B.length b >= ivsize}
 (* MK: minimal cipher length twice blocksize? *)