diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide/coq-ssreflect.lang | 2 | ||||
| -rw-r--r-- | ide/coqide/coq.lang | 2 | ||||
| -rw-r--r-- | ide/coqide/coq.ml | 6 | ||||
| -rw-r--r-- | ide/coqide/coq_commands.ml | 2 | ||||
| -rw-r--r-- | ide/coqide/coqide_ui.ml | 2 | ||||
| -rw-r--r-- | ide/coqide/dune | 3 | ||||
| -rw-r--r-- | ide/coqide/idetop.ml | 1 | ||||
| -rw-r--r-- | ide/coqide/index.mld | 3 | ||||
| -rw-r--r-- | ide/coqide/preferences.ml | 2 |
9 files changed, 14 insertions, 9 deletions
diff --git a/ide/coqide/coq-ssreflect.lang b/ide/coqide/coq-ssreflect.lang index fc7bc64a68..d71277f42c 100644 --- a/ide/coqide/coq-ssreflect.lang +++ b/ide/coqide/coq-ssreflect.lang @@ -32,7 +32,7 @@ <define-regex id="qualit">(\%{ident}*\.)*\%{ident}</define-regex> <define-regex id="undotted_sep">[-+*{}]</define-regex> <define-regex id="dot_sep">\.(\s|\z)</define-regex> - <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex> + <define-regex id="single_decl">(Definition)|(Let)|(Example)|(SubClass)|(Fixpoint)|(CoFixpoint)|(Scheme)|(Function)|(Hypothesis)|(Axiom)|(Variable)|(Parameter)|(Conjecture)|(Inductive)|(CoInductive)|(Variant)|(Record)|(Structure)|(Ltac)|(Instance)|(Context)|(Class)|(Module(\%{space}+Type)?)|(Existing\%{space}+Instance)|(Canonical\%{space}+Structure)|(Canonical)|(Coercion)</define-regex> <define-regex id="mult_decl">(Hypotheses)|(Axioms)|(Variables)|(Parameters)|(Implicit\%{space}+Type(s)?)</define-regex> <define-regex id="locality">(((Local)|(Global))\%{space}+)?</define-regex> <define-regex id="begin_proof">(Theorem)|(Lemma)|(Fact)|(Remark)|(Corollary)|(Proposition)|(Property)</define-regex> diff --git a/ide/coqide/coq.lang b/ide/coqide/coq.lang index e9eab48de7..e6e813aca2 100644 --- a/ide/coqide/coq.lang +++ b/ide/coqide/coq.lang @@ -29,7 +29,7 @@ <define-regex id="qualit">(\%{ident}\.)*\%{ident}</define-regex> <define-regex id="dot_sep">\.(\s|\z)</define-regex> <define-regex id="bullet">([-+*]+|{)(\s|\z)|}(\s*})*</define-regex> - <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe</define-regex> + <define-regex id="single_decl">Definition|Let|Example|SubClass|(Co)?Fixpoint|Function|Conjecture|(Co)?Inductive|Variant|Record|Structure|Ltac|Instance|Class|Existing\%{space}Instance|Canonical\%{space}Structure|Coercion|Universe</define-regex> <define-regex id="mult_decl">Hypothes[ie]s|Axiom(s)?|Variable(s)?|Parameter(s)?|Context|Implicit\%{space}Type(s)?</define-regex> <define-regex id="locality">((Local|Global)\%{space})?</define-regex> <define-regex id="begin_proof">Theorem|Lemma|Fact|Remark|Corollary|Proposition|Property</define-regex> 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/coq_commands.ml b/ide/coqide/coq_commands.ml index 2d75ad9ff6..3a080d5f51 100644 --- a/ide/coqide/coq_commands.ml +++ b/ide/coqide/coq_commands.ml @@ -93,7 +93,6 @@ let commands = [ ]; ["Read Module"; "Record"; - "Variant"; "Remark"; "Remove LoadPath"; "Remove Printing Constructor"; @@ -151,6 +150,7 @@ let commands = [ "Unset Silent."; "Unset Undo";]; ["Variable"; + "Variant"; "Variables";]; ["Write State";]; ] 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' />\ diff --git a/ide/coqide/dune b/ide/coqide/dune index 4bb4672cd4..d2642f77bf 100644 --- a/ide/coqide/dune +++ b/ide/coqide/dune @@ -51,6 +51,9 @@ (modes exe byte) (libraries coqide_gui)) +(documentation + (package coqide)) + ; Input-method bindings (executable (name default_bindings_src) diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 2fe57ec66c..0a0b932c46 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -177,7 +177,6 @@ let concl_next_tac = "symmetry" ] @ [ "assumption"; - "omega"; "ring"; "auto"; "eauto"; diff --git a/ide/coqide/index.mld b/ide/coqide/index.mld new file mode 100644 index 0000000000..8852a2a7eb --- /dev/null +++ b/ide/coqide/index.mld @@ -0,0 +1,3 @@ +{0 coqide } + +The coqide package only contains the CoqIDE executable and no OCaml library. diff --git a/ide/coqide/preferences.ml b/ide/coqide/preferences.ml index 5a77f4ebcf..8361cc3940 100644 --- a/ide/coqide/preferences.ml +++ b/ide/coqide/preferences.ml @@ -304,7 +304,7 @@ let encoding = new preference ~name:["encoding"] ~init ~repr let automatic_tactics = - let init = ["trivial"; "tauto"; "auto"; "omega"; "auto with *"; "intuition" ] in + let init = ["trivial"; "tauto"; "auto"; "auto with *"; "intuition" ] in new preference ~name:["automatic_tactics"] ~init ~repr:Repr.(string_list) let cmd_print = |