diff options
| author | Maxime Dénès | 2019-02-18 23:10:28 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-18 23:10:28 +0100 |
| commit | 582ba8464962f69f0808ccdd14e7bd64e786875f (patch) | |
| tree | 250229466de145992b823fd36f7bf7cd8560f2a9 /doc | |
| parent | 7c62153610f54a96cdded0455af0fff7ff91a53a (diff) | |
| parent | 723f4434d7c715630533031f1bb1522d5d933ce5 (diff) | |
Merge PR #9306: Remove Printing Primitive Projection Compatibility
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 933f07674a..d2fd08536a 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -247,11 +247,6 @@ Primitive Projections printing time (even though they are absent in the actual AST manipulated by the kernel). -.. flag:: Printing Primitive Projection Compatibility - - This compatibility option (on by default) governs the - printing of pattern matching over primitive records. - Primitive Record Types ++++++++++++++++++++++ @@ -297,8 +292,8 @@ the folded version delta-reduces to the unfolded version. This allows to precisely mimic the usual unfolding rules of constants. Projections obey the usual ``simpl`` flags of the ``Arguments`` command in particular. There is currently no way to input unfolded primitive projections at the -user-level, and one must use the :flag:`Printing Primitive Projection Compatibility` -to display unfolded primitive projections as matches and distinguish them from folded ones. +user-level, and there is no way to display unfolded projections differently +from folded ones. Compatibility Projections and :g:`match` |