diff options
| author | Gaëtan Gilbert | 2019-01-04 16:16:11 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-10 16:58:05 +0100 |
| commit | 723f4434d7c715630533031f1bb1522d5d933ce5 (patch) | |
| tree | e8dc22422765b7428b29e0634d93e065c87b50c1 /doc | |
| parent | 2eae13f396833e582697be6a0b3513fc169b8053 (diff) | |
Remove Printing Primitive Projection Compatibility
The code to generate the legacy bodies is moved to its only user in
extraction.
It almost seems like we could remove it (ie no special extraction code
for primitive projection constants) but then we run into issues with
automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets
extracted to `type foo = nat` and (if we remove the special code) `let
a = a`.
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 376a6b8eed..dec4b1a38a 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -246,11 +246,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 ++++++++++++++++++++++ @@ -296,8 +291,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` |