diff options
author | 2017-11-19 22:53:28 +0100 | |
---|---|---|
committer | 2017-11-28 12:31:33 +0100 | |
commit | 0ad26633a4589d77de1f864733d1d953dab9ea91 (patch) | |
tree | 6a29523cc21038de964a935ff24c2c634b8c06eb /vernac | |
parent | f303ed9fb26797b9ec7d172fe583e7ee607ae441 (diff) |
Fix (partial) #4878: option to stop autodeclaring axiom as instance.
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/command.ml | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 373e5a1be..01c7f149b 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -174,6 +174,24 @@ let do_definition ident k univdecl bl red_option c ctypopt hook = (* 2| Variable/Hypothesis/Parameter/Axiom declarations *) +let axiom_into_instance = ref false + +let _ = + let open Goptions in + declare_bool_option + { optdepr = false; + optname = "automatically declare axioms whose type is a typeclass as instances"; + optkey = ["Typeclasses";"Axioms";"Are";"Instances"]; + optread = (fun _ -> !axiom_into_instance); + optwrite = (:=) axiom_into_instance; } + +let should_axiom_into_instance = function + | Discharge -> + (* The typeclass behaviour of Variable and Context doesn't depend + on section status *) + true + | Global | Local -> !axiom_into_instance + let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = match local with | Discharge when Lib.sections_are_opened () -> @@ -195,6 +213,7 @@ match local with (r,Univ.Instance.empty,true) | Global | Local | Discharge -> + let do_instance = should_axiom_into_instance local in let local = DeclareDef.get_locality ident ~kind:"axiom" local in let inl = match nl with | NoInline -> None @@ -207,7 +226,7 @@ match local with let () = maybe_declare_manual_implicits false gr imps in let () = Universes.register_universe_binders gr pl in let () = assumption_message ident in - let () = Typeclasses.declare_instance None false gr in + let () = if do_instance then Typeclasses.declare_instance None false gr in let () = if is_coe then Class.try_add_new_coercion gr ~local p in let inst = match ctx with | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx |