diff options
| author | Clément Pit-Claudel | 2018-05-18 01:49:13 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | f39626edcbd56bd7b05aabe8b60e9af72d27bbfd (patch) | |
| tree | 5691a656af716c184d0878097e294fbb103d0004 | |
| parent | 145da17e8312a7963229e36ef7b1448299357117 (diff) | |
[doc] Fix a few syntax highlighting issues
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 5eba539e03..403b163196 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -123,10 +123,10 @@ parameters is any term :math:`f \, t_1 \ldots t_n`. .. coqtop:: in - forall (A : Type) (S1 S1’ S2 S2’ : list A), - set_eq A S1 S1’ -> - set_eq A S2 S2’ -> - set_eq A (union A S1 S2) (union A S1’ S2’). + forall (A: Type) (S1 S1' S2 S2': list A), + set_eq A S1 S1' -> + set_eq A S2 S2' -> + set_eq A (union A S1 S2) (union A S1' S2'). The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A`` for all ``A``. @@ -448,7 +448,7 @@ various combinations of properties on relations and morphisms are represented as records and instances of theses classes are put in a hint database. For example, the declaration: -.. coqtop:: in +.. coqdoc:: Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m) [reflexivity proved by refl] @@ -459,7 +459,7 @@ hint database. For example, the declaration: is equivalent to an instance declaration: -.. coqtop:: in +.. coqdoc:: Instance (x1 : T1) ... (xn : Tn) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := [Equivalence_Reflexive := refl] |