diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 4 |
2 files changed, 0 insertions, 15 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index a011c81f15..52e47b52ae 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -135,17 +135,6 @@ use the :g:`dec` combinator to get the correct hypotheses as in: The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not produce an equality, contrary to the let pattern construct :g:`let '(x1,..., xn) := t in b`. -Also, :g:`term :>` explicitly asks the system to -coerce term to its support type. It can be useful in notations, for -example: - -.. coqtop:: all - - Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing). - -This notation denotes equality on subset types using equality on their -support types, avoiding uses of proof-irrelevance that would come up -when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts :cmd:`Definition` and :cmd:`Fixpoint` diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index fcf61a5bf4..1a729ced4e 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -42,7 +42,6 @@ Type cast term_cast ::= @term10 : @type | @term10 <: @type | @term10 <<: @type - | @term10 :> The expression :n:`@term10 : @type` is a type cast expression. It enforces the type of :n:`@term10` to be :n:`@type`. @@ -53,9 +52,6 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`). :n:`@term10 <<: @type` specifies that compilation to OCaml will be used to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`). -:n:`@term10 :>` casts to the support type in Program mode. -See :ref:`syntactic_control`. - .. _gallina-definitions: Top-level definitions |