diff options
| author | Jim Fehrle | 2020-04-01 13:18:03 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-06-08 16:50:53 -0700 |
| commit | 27d6686f399f40904ff6005a84677907d53c5bbf (patch) | |
| tree | 5a27b8acdab8ce79b9a7d10685c8979cda82416b /doc/sphinx/language/core/definitions.rst | |
| parent | 6a76e4394876cb08b02d8e7ea185049147f9cd2b (diff) | |
Convert Ltac chapter to prodn
Diffstat (limited to 'doc/sphinx/language/core/definitions.rst')
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 0e637e5aa3..42203d9d65 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -34,18 +34,18 @@ Type cast .. insertprodn term_cast term_cast .. prodn:: - term_cast ::= @term10 <: @term - | @term10 <<: @term - | @term10 : @term + term_cast ::= @term10 <: @type + | @term10 <<: @type + | @term10 : @type | @term10 :> -The expression :n:`@term : @type` is a type cast expression. It enforces -the type of :n:`@term` to be :n:`@type`. +The expression :n:`@term10 : @type` is a type cast expression. It enforces +the type of :n:`@term10` to be :n:`@type`. -:n:`@term <: @type` locally sets up the virtual machine for checking that -:n:`@term` has type :n:`@type`. +:n:`@term10 <: @type` locally sets up the virtual machine for checking that +:n:`@term10` has type :n:`@type`. -:n:`@term <<: @type` uses native compilation for checking that :n:`@term` +:n:`@term10 <<: @type` uses native compilation for checking that :n:`@term10` has type :n:`@type`. .. _gallina-definitions: |