diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 2 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 78 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 12 | ||||
| -rwxr-xr-x | doc/stdlib/make-library-index | 25 |
8 files changed, 114 insertions, 65 deletions
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index c0a57763b9..5d219ebd0d 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,7 +35,7 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. The tactics solve propositional formulas parameterized by atomic -arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. +arithmetic expressions interpreted over a domain :math:`D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}`. The syntax of the formulas is the following: .. productionlist:: `F` @@ -46,8 +46,8 @@ The syntax of the formulas is the following: where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the operators :math:`−, +, ×` are respectively subtraction, addition, and product; :math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition. -For :math:`\mathbb{Q}`, equality is not Leibniz equality = but the equality of -rationals ==. +For :math:`\mathbb{Q}`, equality is not Leibniz equality ``=`` but the equality of +rationals ``==``. For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the @@ -58,7 +58,7 @@ following expressions: c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c where :math:`z` is a constant in :math:`\mathbb{Z}` and :math:`q` is a constant in :math:`\mathbb{Q}`. -This includes integer constants written using the decimal notation, *i.e.*, c%R. +This includes integer constants written using the decimal notation, *i.e.*, ``c%R``. *Positivstellensatz* refutations @@ -94,7 +94,7 @@ general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False}` and For each conjunct :math:`C_i`, the tactic calls an oracle which searches for :math:`-1` within the cone. Upon success, the oracle returns a *cone -expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`) +expression* that is normalized by the :tacn:`ring` tactic (see :ref:`theringandfieldtacticfamilies`) and checked to be :math:`-1`. `lra`: a decision procedure for linear real and rational arithmetic @@ -245,11 +245,11 @@ proof by abstracting monomials by variables. As shown, such a goal is solved by ``intro x. psatz Z 2.``. The oracle returns the cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2` (polynomial hypotheses are printed in bold). By construction, this expression -belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running `ring` we +belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. .. [#] Support for `nat` and :math:`\mathbb{N}` is obtained by pre-processing the goal with - the `zify` tactic. + the ``zify`` tactic. .. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp .. [#] Variants deal with equalities and strict inequalities. .. [#] In practice, the oracle might fail to produce such a refutation. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 9dae7fd102..391afcb1f7 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2155,6 +2155,12 @@ If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT language, and can be processed by Graphviz tools. The format is unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. +.. cmdv:: Print Universes Subgraph(@names) + +Prints the graph restricted to the requested names (adjusting +constraints to preserve the implied transitive constraints between +kept universes). + .. _existential-variables: Existential variables @@ -2247,7 +2253,3 @@ expression as described in :ref:`ltac`. This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. - -This mechanism is comparable to the ``Declare Implicit Tactic`` command -defined at :ref:`tactics-implicit-automation`, except that the used -tactic is local to each hole instead of being declared globally. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 741f9fe5b0..0b059f92ee 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -758,18 +758,6 @@ Controlling the effect of proof editing commands available hypotheses. -.. flag:: Automatic Introduction - - This option controls the way binders are handled - in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the - option is on, which is the default, binders are automatically put in - the local context of the goal to prove. - - When the option is off, binders are discharged on the statement to be - proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) - has to be used to move the assumptions to the local context. - - .. flag:: Nested Proofs Allowed When turned on (it is off by default), this option enables support for nested diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 457f9b2efa..041f1bc966 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3745,32 +3745,6 @@ Setting implicit automation tactics Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - .. cmd:: Declare Implicit Tactic @tactic - - This command declares a tactic to be used to solve implicit arguments - that Coq does not know how to solve by unification. It is used every - time the term argument of a tactic has one of its holes not fully - resolved. - - .. deprecated:: 8.9 - - This command is deprecated. Use :ref:`typeclasses <typeclasses>` or - :ref:`tactics-in-terms <tactics-in-terms>` instead. - - .. example:: - - .. coqtop:: all - - Parameter quo : nat -> forall n:nat, n<>0 -> nat. - Notation "x // y" := (quo x y _) (at level 40). - Declare Implicit Tactic assumption. - Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. - intros. - exists (n // m). - - The tactic ``exists (n // m)`` did not fail. The hole was solved - by ``assumption`` so that it behaved as ``exists (quo n m H)``. - .. _decisionprocedures: Decision procedures diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index eacd7b4676..8f76085d88 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -167,7 +167,7 @@ Combined Scheme Combined Scheme tree_forest_mutind from tree_forest_ind,forest_tree_ind. - The type of tree_forest_mutrec will be: + The type of tree_forest_mutind will be: .. coqtop:: all diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 8b13789179..b58148ffff 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -1 +1,77 @@ - +plugins/btauto/Algebra.v +plugins/btauto/Btauto.v +plugins/btauto/Reflect.v +plugins/derive/Derive.v +plugins/extraction/ExtrHaskellBasic.v +plugins/extraction/ExtrHaskellNatInt.v +plugins/extraction/ExtrHaskellNatInteger.v +plugins/extraction/ExtrHaskellNatNum.v +plugins/extraction/ExtrHaskellString.v +plugins/extraction/ExtrHaskellZInt.v +plugins/extraction/ExtrHaskellZInteger.v +plugins/extraction/ExtrHaskellZNum.v +plugins/extraction/ExtrOcamlBasic.v +plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOcamlIntConv.v +plugins/extraction/ExtrOcamlNatBigInt.v +plugins/extraction/ExtrOcamlNatInt.v +plugins/extraction/ExtrOcamlString.v +plugins/extraction/ExtrOcamlZBigInt.v +plugins/extraction/ExtrOcamlZInt.v +plugins/extraction/Extraction.v +plugins/funind/FunInd.v +plugins/funind/Recdef.v +plugins/ltac/Ltac.v +plugins/micromega/Env.v +plugins/micromega/EnvRing.v +plugins/micromega/Fourier.v +plugins/micromega/Fourier_util.v +plugins/micromega/Lia.v +plugins/micromega/Lqa.v +plugins/micromega/Lra.v +plugins/micromega/MExtraction.v +plugins/micromega/OrderedRing.v +plugins/micromega/Psatz.v +plugins/micromega/QMicromega.v +plugins/micromega/RMicromega.v +plugins/micromega/Refl.v +plugins/micromega/RingMicromega.v +plugins/micromega/Tauto.v +plugins/micromega/VarMap.v +plugins/micromega/ZCoeff.v +plugins/micromega/ZMicromega.v +plugins/nsatz/Nsatz.v +plugins/omega/Omega.v +plugins/omega/OmegaLemmas.v +plugins/omega/OmegaPlugin.v +plugins/omega/OmegaTactic.v +plugins/omega/PreOmega.v +plugins/quote/Quote.v +plugins/romega/ROmega.v +plugins/romega/ReflOmegaCore.v +plugins/rtauto/Bintree.v +plugins/rtauto/Rtauto.v +plugins/setoid_ring/Algebra_syntax.v +plugins/setoid_ring/ArithRing.v +plugins/setoid_ring/BinList.v +plugins/setoid_ring/Cring.v +plugins/setoid_ring/Field.v +plugins/setoid_ring/Field_tac.v +plugins/setoid_ring/Field_theory.v +plugins/setoid_ring/InitialRing.v +plugins/setoid_ring/Integral_domain.v +plugins/setoid_ring/NArithRing.v +plugins/setoid_ring/Ncring.v +plugins/setoid_ring/Ncring_initial.v +plugins/setoid_ring/Ncring_polynom.v +plugins/setoid_ring/Ncring_tac.v +plugins/setoid_ring/RealField.v +plugins/setoid_ring/Ring.v +plugins/setoid_ring/Ring_base.v +plugins/setoid_ring/Ring_polynom.v +plugins/setoid_ring/Ring_tac.v +plugins/setoid_ring/Ring_theory.v +plugins/setoid_ring/Rings_Q.v +plugins/setoid_ring/Rings_R.v +plugins/setoid_ring/Rings_Z.v +plugins/setoid_ring/ZArithRing.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index e8f6decfbf..4fc9bf9e19 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -571,6 +571,7 @@ through the <tt>Require Import</tt> command.</p> theories/Reals/Sqrt_reg.v theories/Reals/Rlogic.v (theories/Reals/Reals.v) + theories/Reals/Runcountable.v </dd> <dt> <b>Program</b>: @@ -588,6 +589,17 @@ through the <tt>Require Import</tt> command.</p> theories/Program/Combinators.v </dd> + <dt> <b>SSReflect</b>: + Base libraries for the SSReflect proof language and the + small scale reflection formalization technique + </dt> + <dd> + plugins/ssrmatching/ssrmatching.v + plugins/ssr/ssreflect.v + plugins/ssr/ssrbool.v + plugins/ssr/ssrfun.v + </dd> + <dt> <b>Unicode</b>: Unicode-based notations </dt> diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index index 43802efa0a..bea6f24098 100755 --- a/doc/stdlib/make-library-index +++ b/doc/stdlib/make-library-index @@ -8,35 +8,32 @@ HIDDEN=$2 cp -f $FILE.template tmp echo -n "Building file index-list.prehtml... " -#LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings" -LIBDIRS=`find theories/* -type d ! -name .coq-native | sed -e "s:^theories/::"` +LIBDIRS=`find theories/* plugins/* -type d ! -name .coq-native` for k in $LIBDIRS; do - i=theories/$k - d=`basename $i` - ls $i | grep -q \.v'$' + d=`basename $k` + ls $k | grep -q \.v'$' if [ $? = 0 ]; then - for j in $i/*.v; do + for j in $k/*.v; do b=`basename $j .v` rm -f tmp2 - grep -q theories/$k/$b.v tmp + grep -q $k/$b.v tmp a=$? - grep -q theories/$k/$b.v $HIDDEN + grep -q $k/$b.v $HIDDEN h=$? if [ $a = 0 ]; then if [ $h = 0 ]; then - echo Error: $FILE and $HIDDEN both mention theories/$k/$b.v; exit 1 + echo Error: $FILE and $HIDDEN both mention $k/$b.v; exit 1 else - p=`echo $k | sed 's:/:.:g'` - sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 + p=`echo $k | sed 's:^[^/]*/::' | sed 's:/:.:g'` + sed -e "s:$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2 mv -f tmp2 tmp fi else if [ $h = 0 ]; then - echo Error: theories/$k/$b.v is missing in the template file - exit 1 + echo Warning: $k/$b.v will be hidden from the index else - echo Error: none of $FILE and $HIDDEN mention theories/$k/$b.v + echo Error: none of $FILE and $HIDDEN mention $k/$b.v exit 1 fi |