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.
---
 interp/dumpglob.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index a537b4848c..274f9b851a 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -91,7 +91,8 @@ let type_of_logical_kind = function
       (match a with
       | Definitional -> "defax"
       | Logical -> "prfax"
-      | Conjectural -> "prfax")
+      | Conjectural -> "prfax"
+      | Context -> "prfax")
   | IsProof th ->
       (match th with
       | Theorem
-- 
cgit v1.2.3