diff options
| author | Théo Zimmermann | 2019-02-16 16:03:11 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 21:24:11 +0100 |
| commit | b16cea4007e4286d596a46bce80815939bca271d (patch) | |
| tree | 3c4eab3e78c364e21fa88a6d610d14846547518c /doc/sphinx/addendum | |
| parent | ea8a9125a4e81e7c848cf53f1e34f534d359e832 (diff) | |
Using options abort and restart of coqtop directive in the manual.
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 |