diff options
| author | Pierre-Marie Pédrot | 2021-04-08 13:32:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-04-08 13:32:09 +0200 |
| commit | 2b8d8b996b7ae9b5c170792cbf45c4fd96ed3658 (patch) | |
| tree | f9c66fdb5c46a5ebee954fbc3bf61d74163a1611 | |
| parent | 59d0462f35818c12a0727a560d7b9ecf2ceea994 (diff) | |
| parent | 1fdc02ef7bf0b3d98eb2c69ab5cf8cd84f77b668 (diff) | |
Merge PR #14062: Fixes #11690: wrongly toggled coqide printing matching flag
Reviewed-by: ppedrot
| -rw-r--r-- | ide/coqide/coq.ml | 6 | ||||
| -rw-r--r-- | ide/coqide/coqide_ui.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 20e9f0134f..dc616066c2 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -538,7 +538,7 @@ struct let implicit = BoolOpt ["Printing"; "Implicit"] let coercions = BoolOpt ["Printing"; "Coercions"] - let raw_matching = BoolOpt ["Printing"; "Matching"] + let nested_matching = BoolOpt ["Printing"; "Matching"] let notations = BoolOpt ["Printing"; "Notations"] let parentheses = BoolOpt ["Printing"; "Parentheses"] let all_basic = BoolOpt ["Printing"; "All"] @@ -553,8 +553,8 @@ struct let bool_items = [ { opts = [implicit]; init = false; label = "Display _implicit arguments" }; { opts = [coercions]; init = false; label = "Display _coercions" }; - { opts = [raw_matching]; init = true; - label = "Display raw _matching expressions" }; + { opts = [nested_matching]; init = true; + label = "Display nested _matching expressions" }; { opts = [notations]; init = true; label = "Display _notations" }; { opts = [parentheses]; init = false; label = "Display _parentheses" }; { opts = [all_basic]; init = false; diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml index badfabf07e..82eca905ea 100644 --- a/ide/coqide/coqide_ui.ml +++ b/ide/coqide/coqide_ui.ml @@ -77,7 +77,7 @@ let init () = \n <separator/>\ \n <menuitem action='Display implicit arguments' />\ \n <menuitem action='Display coercions' />\ -\n <menuitem action='Display raw matching expressions' />\ +\n <menuitem action='Display nested matching expressions' />\ \n <menuitem action='Display notations' />\ \n <menuitem action='Display parentheses' />\ \n <menuitem action='Display all basic low-level contents' />\ |