diff options
| author | Hugo Herbelin | 2015-01-24 20:41:13 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-24 21:48:44 +0100 |
| commit | 982b583efe9f657d76b4257200769fed55453623 (patch) | |
| tree | f225282ac8a6c38dac72ae452d5139511d624aea | |
| parent | ef61bb05911d19c77d565d78dc57107d40c333e4 (diff) | |
Equality Schemes options: reverting commit ff9f94634 which is
obviously inconsistent with the decisions taken in commits
2e8fb20e04da and 0bc569026048 about bugs #2550 and #3606.
Now having options Boolean Equality Schemes and Decidable Equality Schemes.
| -rw-r--r-- | toplevel/indschemes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index e6b2382867..fbc45b4ae3 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -85,7 +85,7 @@ let _ = { optsync = true; optdepr = false; optname = "automatic declaration of boolean equality"; - optkey = ["Equality";"Schemes"]; + optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } let _ = (* compatibility *) |