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.

4 files changed, 9 insertions, 6 deletions

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
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]
 
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index c37e90650a..49f32dd401 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -37,11 +37,11 @@ let () =
       optwrite = (:=) axiom_into_instance; }
 
 let should_axiom_into_instance = function
-  | Discharge ->
+  | Context ->
     (* The typeclass behaviour of Variable and Context doesn't depend
        on section status *)
     true
-  | Global | Local -> !axiom_into_instance
+  | Definitional | Logical | Conjectural -> !axiom_into_instance
 
 let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
 match local with
@@ -62,7 +62,7 @@ match local with
   (r,Univ.Instance.empty,true)
 
 | Global | Local | Discharge ->
-  let do_instance = should_axiom_into_instance local in
+  let do_instance = should_axiom_into_instance kind in
   let local = DeclareDef.get_locality ident ~kind:"axiom" local in
   let inl = let open Declaremods in match nl with
     | NoInline -> None
@@ -288,7 +288,7 @@ let context poly l =
       | _ -> false
       in
       let impl = List.exists test impls in
-      let decl = (Discharge, poly, Definitional) in
+      let decl = (Discharge, poly, Context) in
       let nstatus = match b with
       | None ->
         pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 02af1904fd..fda1e2afea 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -359,6 +359,8 @@ open Pputils
         keyword (if many then "Variables" else "Variable")
       | (DoDischarge,Conjectural) ->
         anomaly (Pp.str "Don't know how to beautify a local conjecture.")
+      | (_,Context) ->
+        anomaly (Pp.str "Context is used only internally.")
 
   let pr_params pr_c (xl,(c,t)) =
     hov 2 (prlist_with_sep sep pr_lident xl ++ spc() ++