From b23c3fee91e146d4aa2bc2c75ea30619a204c3d9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 12 Oct 2018 20:02:57 +0200
Subject: Adding a new kind of assumption to track assumption coming from
 "Context".

This is to avoid depending on the combination "Discharge" + no opened
section to trigger an automatic declaration of instance.
---
 library/decl_kinds.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 8d5c2fb687..8decdbea1e 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -46,7 +46,7 @@ type definition_object_kind =
   | Method
   | Let
 
-type assumption_object_kind = Definitional | Logical | Conjectural
+type assumption_object_kind = Definitional | Logical | Conjectural | Context
 
 (* [assumption_kind]
 
-- 
cgit v1.2.3