aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/04-tactics/13781-deprecate_micromega_options.rst3
-rw-r--r--doc/sphinx/addendum/micromega.rst6
-rw-r--r--doc/sphinx/language/core/assumptions.rst2
-rw-r--r--doc/sphinx/proofs/writing-proofs/rewriting.rst59
-rw-r--r--doc/tools/docgram/common.edit_mlg4
-rw-r--r--doc/tools/docgram/fullGrammar15
-rw-r--r--doc/tools/docgram/orderedGrammar18
7 files changed, 61 insertions, 46 deletions
diff --git a/doc/changelog/04-tactics/13781-deprecate_micromega_options.rst b/doc/changelog/04-tactics/13781-deprecate_micromega_options.rst
new file mode 100644
index 0000000000..e3375bd875
--- /dev/null
+++ b/doc/changelog/04-tactics/13781-deprecate_micromega_options.rst
@@ -0,0 +1,3 @@
+- **Deprecated:**
+ The micromega option :flag:`Simplex`, which is currently set by default
+ (`#13781 <https://github.com/coq/coq/pull/13781>`_, by Frédéric Besson).
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 3bd85d29c8..5d471c695c 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -31,9 +31,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`,
.. flag:: Simplex
+ .. deprecated:: 8.14
+
This flag (set by default) instructs the decision procedures to
- use the Simplex method for solving linear goals. If it is not set,
- the decision procedures are using Fourier elimination.
+ use the Simplex method for solving linear goals instead of the
+ deprecated Fourier elimination.
.. opt:: Dump Arith
diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst
index 8dbc1626ba..7566996ef6 100644
--- a/doc/sphinx/language/core/assumptions.rst
+++ b/doc/sphinx/language/core/assumptions.rst
@@ -9,7 +9,7 @@ Binders
.. insertprodn open_binders binder
.. prodn::
- open_binders ::= {+ @name } : @term
+ open_binders ::= {+ @name } : @type
| {+ @binder }
name ::= _
| @ident
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 663337bc64..f286533d78 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -44,11 +44,14 @@ Rewriting with Leibniz and setoid equality
oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings
one_term_with_bindings ::= {? > } @one_term {? with @bindings }
- Rewrites terms based on equalities. The type of :n:`@one_term` must have the form:
+ Replaces subterms with other subterms that have been proven to be equal.
+ The type of :n:`@one_term` must have the form:
:n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2`
- where :g:`EQ` is the Leibniz equality `eq` or a registered setoid equality.
+ .. todo :term:`Leibniz equality` does not work with Sphinx 2.3.1. It does with Sphinx 3.0.3.
+
+ where :g:`EQ` is the Leibniz equality `eq` or a registered :term:`setoid equality`.
Note that :n:`eq @term__1 @term__2` is typically written with the infix notation
:n:`@term__1 = @term__2`. You must `Require Setoid` to use the tactic
with a setoid equality or with :ref:`setoid rewriting <generalizedrewriting>`.
@@ -61,7 +64,7 @@ Rewriting with Leibniz and setoid equality
Some of the variables :g:`x`\ :sub:`i` are solved by unification,
and some of the types :n:`A__1, ..., A__n` may become new
subgoals. :tacn:`rewrite` won't find occurrences inside `forall` that refer
- to variables bound by the `forall`; use :tacn:`setoid_rewrite`
+ to variables bound by the `forall`; use the more advanced :tacn:`setoid_rewrite`
if you want to find such occurrences.
:n:`{+, @oriented_rewriter }`
@@ -90,15 +93,55 @@ Rewriting with Leibniz and setoid equality
any of them can be rewritten. If not specified, only the first occurrence
in the conclusion is replaced.
- If :n:`at @occs_nums` is specified, rewriting is always done with
- :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality,
- which means that you must `Require Setoid` to use that form.
- However, note that :tacn:`rewrite` (even when using setoid rewriting) and
- :tacn:`setoid_rewrite` don't behave identically (as already mentioned above).
+ .. note::
+
+ If :n:`at @occs_nums` is specified, rewriting is always done
+ with :ref:`setoid rewriting <generalizedrewriting>`, even for
+ Leibniz equality, which means that you must `Require
+ Setoid` to use that form. However, note that :tacn:`rewrite`
+ (even when using setoid rewriting) and :tacn:`setoid_rewrite`
+ don't behave identically (as is noted above and below).
:n:`by @ltac_expr3`
If specified, is used to resolve all side conditions generated by the tactic.
+ .. note::
+
+ For each selected hypothesis and/or the conclusion,
+ :tacn:`rewrite` finds the first matching subterm in
+ depth-first search order. Only subterms identical to
+ that first matched subterm are rewritten. If the `at` clause is specified,
+ only these subterms are considered when counting occurrences.
+ To select a different set of matching subterms, you can
+ specify how some or all of the free variables are bound by
+ using a `with` clause (see :n:`@one_term_with_bindings`).
+
+ For instance, if we want to rewrite the right-hand side in the
+ following goal, this will not work:
+
+ .. coqtop:: none
+
+ Require Import Arith.
+
+ .. coqtop:: out
+
+ Lemma example x y : x + y = y + x.
+
+ .. coqtop:: all fail
+
+ rewrite Nat.add_comm at 2.
+
+ One can explicitly specify how some variables are bound to match
+ a different subterm:
+
+ .. coqtop:: all abort
+
+ rewrite Nat.add_comm with (m := x).
+
+ Note that the more advanced :tacn:`setoid_rewrite` tactic
+ behaves differently, and thus the number of occurrences
+ available to rewrite may differ between the two tactics.
+
.. exn:: Tactic failure: Setoid library not loaded.
:undocumented:
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 8aeb2e564d..27144fd1ad 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -447,7 +447,7 @@ binder: [
open_binders: [
| REPLACE name LIST0 name ":" lconstr
-| WITH LIST1 name ":" lconstr
+| WITH LIST1 name ":" type
(* @Zimmi48: Special token .. is for use in the Notation command. (see bug_3304.v) *)
| DELETE name ".." name
| REPLACE name LIST0 name binders
@@ -1510,8 +1510,6 @@ query_command: [
| WITH "Check" lconstr
| REPLACE "About" smart_global OPT univ_name_list "."
| WITH "About" smart_global OPT univ_name_list
-| REPLACE "SearchHead" constr_pattern in_or_out_modules "."
-| WITH "SearchHead" constr_pattern in_or_out_modules
| REPLACE "SearchPattern" constr_pattern in_or_out_modules "."
| WITH "SearchPattern" constr_pattern in_or_out_modules
| REPLACE "SearchRewrite" constr_pattern in_or_out_modules "."
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ec23ffe83e..bc6b803bbb 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -687,17 +687,6 @@ command: [
| "Add" "Zify" "BinOpSpec" constr (* micromega plugin *)
| "Add" "Zify" "UnOpSpec" constr (* micromega plugin *)
| "Add" "Zify" "Saturate" constr (* micromega plugin *)
-| "Add" "InjTyp" constr (* micromega plugin *)
-| "Add" "BinOp" constr (* micromega plugin *)
-| "Add" "UnOp" constr (* micromega plugin *)
-| "Add" "CstOp" constr (* micromega plugin *)
-| "Add" "BinRel" constr (* micromega plugin *)
-| "Add" "PropOp" constr (* micromega plugin *)
-| "Add" "PropBinOp" constr (* micromega plugin *)
-| "Add" "PropUOp" constr (* micromega plugin *)
-| "Add" "BinOpSpec" constr (* micromega plugin *)
-| "Add" "UnOpSpec" constr (* micromega plugin *)
-| "Add" "Saturate" constr (* micromega plugin *)
| "Show" "Zify" "InjTyp" (* micromega plugin *)
| "Show" "Zify" "BinOp" (* micromega plugin *)
| "Show" "Zify" "UnOp" (* micromega plugin *)
@@ -705,7 +694,6 @@ command: [
| "Show" "Zify" "BinRel" (* micromega plugin *)
| "Show" "Zify" "UnOpSpec" (* micromega plugin *)
| "Show" "Zify" "BinOpSpec" (* micromega plugin *)
-| "Show" "Zify" "Spec" (* micromega plugin *)
| "Add" "Ring" ident ":" constr OPT ring_mods (* ring plugin *)
| "Print" "Rings" (* ring plugin *)
| "Add" "Field" ident ":" constr OPT field_mods (* ring plugin *)
@@ -1258,7 +1246,6 @@ query_command: [
| "Compute" lconstr "."
| "Check" lconstr "."
| "About" smart_global OPT univ_name_list "."
-| "SearchHead" constr_pattern in_or_out_modules "."
| "SearchPattern" constr_pattern in_or_out_modules "."
| "SearchRewrite" constr_pattern in_or_out_modules "."
| "Search" search_query search_queries "."
@@ -1551,7 +1538,6 @@ simple_tactic: [
| "revert" LIST1 hyp
| "simple" "induction" quantified_hypothesis
| "simple" "destruct" quantified_hypothesis
-| "double" "induction" quantified_hypothesis quantified_hypothesis
| "admit"
| "fix" ident natural
| "cofix" ident
@@ -1669,7 +1655,6 @@ simple_tactic: [
| "autounfold_one" hintbases
| "unify" constr constr
| "unify" constr constr "with" preident
-| "convert_concl_no_check" constr
| "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident
| "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident
| "typeclasses" "eauto" "bfs" OPT nat_or_var
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 75b32a5800..a34e96ac16 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -493,7 +493,7 @@ term_forall_or_fun: [
]
open_binders: [
-| LIST1 name ":" term
+| LIST1 name ":" type
| LIST1 binder
]
@@ -1001,18 +1001,6 @@ command: [
| "Reset" "Ltac" "Profile"
| "Show" "Ltac" "Profile" OPT [ "CutOff" integer | string ]
| "Show" "Lia" "Profile" (* micromega plugin *)
-| "Add" "InjTyp" one_term (* micromega plugin *)
-| "Add" "BinOp" one_term (* micromega plugin *)
-| "Add" "UnOp" one_term (* micromega plugin *)
-| "Add" "CstOp" one_term (* micromega plugin *)
-| "Add" "BinRel" one_term (* micromega plugin *)
-| "Add" "PropOp" one_term (* micromega plugin *)
-| "Add" "PropBinOp" one_term (* micromega plugin *)
-| "Add" "PropUOp" one_term (* micromega plugin *)
-| "Add" "BinOpSpec" one_term (* micromega plugin *)
-| "Add" "UnOpSpec" one_term (* micromega plugin *)
-| "Add" "Saturate" one_term (* micromega plugin *)
-| "Show" "Zify" "Spec" (* micromega plugin *)
| "Add" "Ring" ident ":" one_term OPT ( "(" LIST1 ring_mod SEP "," ")" ) (* ring plugin *)
| "Print" "Rings" (* ring plugin *)
| "Add" "Field" ident ":" one_term OPT ( "(" LIST1 field_mod SEP "," ")" ) (* ring plugin *)
@@ -1117,7 +1105,6 @@ command: [
| "Compute" term
| "Check" term
| "About" reference OPT univ_name_list
-| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
@@ -1626,7 +1613,6 @@ simple_tactic: [
| "revert" LIST1 ident
| "simple" "induction" [ ident | natural ]
| "simple" "destruct" [ ident | natural ]
-| "double" "induction" [ ident | natural ] [ ident | natural ]
| "admit"
| "clear" LIST0 ident
| "clear" "-" LIST1 ident
@@ -1758,7 +1744,6 @@ simple_tactic: [
| "autounfold" OPT hintbases OPT occurrences
| "autounfold_one" OPT hintbases OPT ( "in" ident )
| "unify" one_term one_term OPT ( "with" ident )
-| "convert_concl_no_check" one_term
| "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident )
| "head_of_constr" ident one_term
| "not_evar" one_term
@@ -2420,7 +2405,6 @@ tac2mode: [
| "Compute" term
| "Check" term
| "About" reference OPT univ_name_list
-| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 18:00:31 +0000