diff options
| author | Théo Zimmermann | 2019-08-05 23:40:48 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-08-05 23:40:48 +0200 |
| commit | cce00f7a3f0c5fe101b713f32ca4c67ff5970121 (patch) | |
| tree | fa9c6dd73ed390c382198138f7b75a3fcb25d161 /doc | |
| parent | f3d8eb529c43c9509c53f013ff47cc45b3685a6b (diff) | |
| parent | 514a4db2eca54ae8c4c1ba1e081a918528566fce (diff) | |
Merge PR #10624: Remove reference to removed option Printing Primitive Projection Compatibility
Reviewed-by: Zimmi48
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index acf68e9fd2..dc4f91e66b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -260,10 +260,7 @@ To eliminate the (co-)inductive type, one must use its defined primitive project For compatibility, the parameters still appear to the user when printing terms even though they are absent in the actual AST manipulated by the kernel. This can be changed by unsetting the -:flag:`Printing Primitive Projection Parameters` flag. Further compatibility -printing can be deactivated thanks to the ``Printing Primitive Projection -Compatibility`` option which governs the printing of pattern matching -over primitive records. +:flag:`Printing Primitive Projection Parameters` flag. There are currently two ways to introduce primitive records types: |