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_commands.ml | 1 | ||||
| -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 |
7 files changed, 10 insertions, 4 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_commands.ml b/ide/coqide/coq_commands.ml index 2d75ad9ff6..6e02d7fed1 100644 --- a/ide/coqide/coq_commands.ml +++ b/ide/coqide/coq_commands.ml @@ -151,6 +151,7 @@ let commands = [ "Unset Silent."; "Unset Undo";]; ["Variable"; + "Variant"; "Variables";]; ["Write State";]; ] 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 a6a7f7d742..72b54d329f 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 = |