From df122cc2df844de72aca9fcd4896efd648be4210 Mon Sep 17 00:00:00 2001
From: Florian Deljarry <deljarry.florian@gmail.com>
Date: Sun, 26 May 2019 13:17:09 -0400
Subject: [PATCH] check_annotation: adding no_contract

Adding option to remove contract on a specific annotated method

Signed-off-by: Florian Deljarry <deljarry.florian@gmail.com>
---
 src/frontend/check_annotation.nit |    1 +
 1 file changed, 1 insertion(+)

diff --git a/src/frontend/check_annotation.nit b/src/frontend/check_annotation.nit
index b04c498..41ed278 100644
--- a/src/frontend/check_annotation.nit
+++ b/src/frontend/check_annotation.nit
@@ -114,6 +114,7 @@ example
 
 expects
 ensures
+no_contract
 """
 
 	# Efficient set build from `primtives_annotations_list`
-- 
1.7.9.5