diff options
| author | Hugo Herbelin | 2018-10-12 20:02:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-08 20:17:41 +0200 |
| commit | b23c3fee91e146d4aa2bc2c75ea30619a204c3d9 (patch) | |
| tree | 0e90eec1d26d541f7a43dcf6dff622ad3c4ab6e0 /vernac/comAssumption.ml | |
| parent | 65f75de6929530252a3235af54a0da56980fa02d (diff) | |
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.
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |