diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 24 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 15 |
2 files changed, 28 insertions, 11 deletions
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 593afa8f20..8c82526f0c 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1422,15 +1422,6 @@ using the keyword :cmd:`Qed`. #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the current asserted statement into an axiom and exit the proof editing mode. -.. [1] - This is similar to the expression “*entry* :math:`\{` sep *entry* - :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* - :math:`)`\ \*” in the syntax of regular expressions. - -.. [2] - Except if the inductive type is empty in which case there is no - equation that can be used to infer the return type. - .. _gallina-attributes: Attributes @@ -1466,12 +1457,14 @@ the following attributes names are recognized: This attribute can trigger the following warnings: .. warn:: Tactic @qualid is deprecated since @string. @string. + :undocumented: .. warn:: Tactic Notation @qualid is deprecated since @string. @string. + :undocumented: -Here are a few examples: +.. example:: -.. coqtop:: all reset + .. coqtop:: all reset From Coq Require Program. #[program] Definition one : nat := S _. @@ -1486,3 +1479,12 @@ Here are a few examples: Proof. now foo. Abort. + +.. [1] + This is similar to the expression “*entry* :math:`\{` sep *entry* + :math:`\}`” in standard BNF, or “*entry* :math:`(` sep *entry* + :math:`)`\ \*” in the syntax of regular expressions. + +.. [2] + Except if the inductive type is empty in which case there is no + equation that can be used to infer the return type. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index be65ff7570..125c4c25a3 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1200,3 +1200,18 @@ scope of their effect. There are four kinds of commands: modifier extends the effect outside the module even when the command occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. + +.. _exposing-constants-to-ocaml-libraries: + +Exposing constants to OCaml libraries +---------------------------------------------------------------- + +.. cmd:: Register @qualid__1 as @qualid__2 + + This command exposes the constant :n:`@qualid__1` to OCaml libraries under + the name :n:`@qualid__2`. This constant can then be dynamically located + calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known + where is the constant defined (file, module, library, etc.). + + Due to its internal nature, this command is not for general use. It is meant + to appear only in standard libraries and in support libraries of plug-ins. |