diff options
| -rw-r--r-- | CHANGES.md | 4 | ||||
| -rw-r--r-- | vernac/comAssumption.ml | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/CHANGES.md b/CHANGES.md index 6bdb63d4d7..5ff90b5123 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -120,6 +120,10 @@ Universes - Added `Print Universes Subgraph` variant of `Print Universes`. Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).` +Misc + +- Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances. + Changes from 8.8.2 to 8.9+beta1 =============================== diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 8707121306..ef28fc2d77 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -29,7 +29,7 @@ let axiom_into_instance = ref false let _ = let open Goptions in declare_bool_option - { optdepr = false; + { optdepr = true; optname = "automatically declare axioms whose type is a typeclass as instances"; optkey = ["Typeclasses";"Axioms";"Are";"Instances"]; optread = (fun _ -> !axiom_into_instance); |