diff options
| author | Gaëtan Gilbert | 2018-11-06 14:41:56 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-22 13:33:22 +0100 |
| commit | a7cf802627a9842862c6290496d73a815ab2f42b (patch) | |
| tree | a059410470ecdcef666df53a36c995ff3b11e090 | |
| parent | 2d0be200ab9a2e3a0ff7b383078aabe70f24dd82 (diff) | |
Deprecate Typeclasses Axioms Are Instances
People should use Declare Instance instead.
| -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); |