diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 22 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 30 | ||||
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 7 |
7 files changed, 50 insertions, 35 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 56f84d0ff0..b410833d25 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -194,14 +194,14 @@ Program Fixpoint The optional order annotation follows the grammar: .. productionlist:: orderannot - order : measure `term` (`term`)? | wf `term` `term` + order : measure `term` [ `term` ] | wf `term` `ident` - + :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on - any subset of the arguments and the optional (parenthesised) term - ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` - to ``lt``. + + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional term + :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R` + to :g:`lt`. - + :g:`wf R x` which is equivalent to :g:`measure x (R)`. + + :g:`wf R x` which is equivalent to :g:`measure x R`. The structural fixpoint operator behaves just like the one of |Coq| (see :cmd:`Fixpoint`), except it may also generate obligations. It works diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 015b84c530..c0c8c2d79c 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -19,6 +19,9 @@ known as strict propositions). To use :math:`\SProp` you must pass initial value depends on whether you used the command line ``-allow-sprop``. +.. exn:: SProp not allowed, you need to Set Allow StrictProp or to use the -allow-sprop command-line-flag. + :undocumented: + .. coqtop:: none Set Allow StrictProp. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index b069cf27f4..a5e9023732 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -433,22 +433,26 @@ few other commands related to typeclasses. .. _TypeclassesTransparent: -Typeclasses Transparent, Typclasses Opaque -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Typeclasses Transparent, Typeclasses Opaque +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses Transparent {+ @ident} This command makes the identifiers transparent during typeclass resolution. + Shortcut for :n:`Hint Transparent {+ @ident } : typeclass_instances`. .. cmd:: Typeclasses Opaque {+ @ident} - Make the identifiers opaque for typeclass search. It is useful when some - constants prevent some unifications and make resolution fail. It is also - useful to declare constants which should never be unfolded during - proof-search, like fixpoints or anything which does not look like an - abbreviation. This can additionally speed up proof search as the typeclass - map can be indexed by such rigid constants (see + Make the identifiers opaque for typeclass search. + Shortcut for :n:`Hint Opaque {+ @ident } : typeclass_instances`. + + It is useful when some constants prevent some unifications and make + resolution fail. It is also useful to declare constants which + should never be unfolded during proof-search, like fixpoints or + anything which does not look like an abbreviation. This can + additionally speed up proof search as the typeclass map can be + indexed by such rigid constants (see :ref:`thehintsdatabasesforautoandeauto`). By default, all constants and local variables are considered transparent. One @@ -458,8 +462,6 @@ type, like: .. coqdoc:: Definition relation A := A -> A -> Prop. -This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. - Settings ~~~~~~~~ diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index eebf1f11e1..bdda35fcc0 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -210,6 +210,13 @@ and ``coqtop``, unless stated otherwise: is intended to be used as a linter for developments that want to be robust to changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems. +:-set *string*: Enable flags and set options. *string* should be + ``Option Name=value``, the value is interpreted according to the + type of the option. For flags ``Option Name`` is equivalent to + ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` + will enable :flag:`Universe Polymorphism`. Note that the quotes are + shell syntax, Coq does not see them. +:-unset *string*: As ``-set`` but used to disable options and flags. :-compat *version*: Attempt to maintain some backward-compatibility with a previous version. :-dump-glob *file*: Dump references for global names in file *file* diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 8346b72cb9..35231610fe 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -144,6 +144,10 @@ Here we describe only few of them. :CAMLFLAGS: can be used to specify additional flags to the |OCaml| compiler, like ``-bin-annot`` or ``-w``.... +:OCAMLWARN: + it contains a default of ``-warn-error +a-3``, useful to modify + this setting; beware this is not recommended for projects in + Coq's CI. :COQC, COQDEP, COQDOC: can be set in order to use alternative binaries (e.g. wrappers) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index afb0239be4..8d9e99b9d5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3830,25 +3830,25 @@ The general command to add a hint to some databases :n:`{+ @ident}` is check with :cmd:`Print HintDb` to verify the current cut expression: .. productionlist:: regexp - e : `ident` hint or instance identifier - : _ any hint - : `e` | `e` disjunction - : `e` `e` sequence - : `e` * Kleene star - : emp empty - : eps epsilon - : ( `e` ) + regexp : `ident` (hint or instance identifier) + : _ (any hint) + : `regexp` | `regexp` (disjunction) + : `regexp` `regexp` (sequence) + : `regexp` * (Kleene star) + : emp (empty) + : eps (epsilon) + : ( `regexp` ) The `emp` regexp does not match any search path while `eps` matches the empty path. During proof search, the path of successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note that Hint Extern’s do not have + list of identifiers for the hints (note that :cmd:`Hint Extern`\’s do not have an associated identifier). Before applying any hint :n:`@ident` the current path `p` extended with :n:`@ident` is matched against the current cut expression `c` associated to the hint database. If matching succeeds, the hint is *not* applied. The - semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the - initial cut expression being `emp`. + semantics of :n:`Hint Cut @regexp` is to set the cut expression + to :n:`c | regexp`, the initial cut expression being `emp`. .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident :name: Hint Mode @@ -3875,7 +3875,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. note:: One can use an ``Extern`` hint with no pattern to do pattern matching on - hypotheses using ``match goal`` with inside the tactic. + hypotheses using ``match goal with`` inside the tactic. Hint databases defined in the Coq standard library @@ -4724,6 +4724,12 @@ Non-logical tactics from the shelf into focus, by appending them to the end of the current list of focused goals. +.. tacn:: unshelve @tactic + :name: unshelve + + Performs :n:`@tactic`, then unshelves existential variables added to the + shelf by the execution of :n:`@tactic`, prepending them to the current goal. + .. tacn:: give_up :name: give_up diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index eaf1b2c2ad..0ade9fdbf5 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -149,13 +149,6 @@ class CoqObject(ObjectDescription): msg = MSG.format(name, self.env.doc2path(objects[name][0])) self.state_machine.reporter.warning(msg, line=self.lineno) - def _warn_if_duplicate_name(self, objects, name): - """Check that two objects in the same domain don't have the same name.""" - if name in objects: - MSG = 'Duplicate object: {}; other is at {}' - msg = MSG.format(name, self.env.doc2path(objects[name][0])) - self.state_machine.reporter.warning(msg, line=self.lineno) - def _record_name(self, name, target_id): """Record a name, mapping it to target_id |