From eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sun, 7 Mar 2021 10:15:11 -0800
Subject: Remove the :> type cast

---
 doc/sphinx/addendum/program.rst | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'doc/sphinx/addendum/program.rst')

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`
-- 
cgit v1.2.3