diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index cc788b3595..b474c51f17 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -627,14 +627,10 @@ logical equivalence: Instance all_iff_morphism (A : Type) : Proper (pointwise_relation A iff ==> iff) (@all A). -.. coqtop:: all +.. coqtop:: all abort Proof. simpl_relation. -.. coqtop:: none - - Abort. - One then has to show that if two predicates are equivalent at every point, their universal quantifications are equivalent. Once we have declared such a morphism, it will be used by the setoid rewriting |