diff options
| author | Théo Zimmermann | 2020-05-14 12:47:26 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-14 12:47:26 +0200 |
| commit | 26cd7d093822556fc919dc7e27cac0196f564fc2 (patch) | |
| tree | 51bacd2d39daf9da9698918f6aa151fa8c676640 /doc/sphinx/language/extensions | |
| parent | 95c4fc791b1eda5357855f706dfdb4c050d6c28e (diff) | |
Add some markers of origin.
Diffstat (limited to 'doc/sphinx/language/extensions')
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/evars.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/match.rst | 2 |
3 files changed, 10 insertions, 0 deletions
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index d97c98da9c..87c9b96a84 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -14,6 +14,8 @@ of another, complementary, use of canonical structures: advanced proof search. This latter papers also presents many techniques one can employ to tune the inference of canonical structures. + .. extracted from implicit arguments section + .. _canonical-structure-declaration: Declaraction of canonical structures diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index 8dc5b99c4d..7635441c24 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -1,3 +1,5 @@ +.. extracted from Gallina extensions chapter + .. _existential-variables: Existential variables @@ -62,6 +64,8 @@ the syntax :n:`?[@ident]`. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. with a named-goal selector, see :ref:`goal-selectors`). +.. extracted from Gallina chapter + .. index:: _ Inferable subterms @@ -71,6 +75,8 @@ Expressions often contain redundant pieces of information. Subterms that can be automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will guess the missing piece of information. +.. extracted from Gallina extensions chapter + .. _explicit-display-existentials: Explicit displaying of existential instances for pretty-printing diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index c5452d4590..b83e11e253 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -9,6 +9,8 @@ This section describes the full form of pattern matching in |Coq| terms. .. |rhs| replace:: right hand sides + .. extracted from Gallina extensions chapter + Variants and extensions of :g:`match` ------------------------------------- |