From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- test-suite/coqdoc/links.html.out | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'test-suite/coqdoc/links.html.out') diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index 5e4b676c..d2d4d5d7 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -60,32 +60,32 @@ Various checks for coqdoc Definition f := ∀ C:Prop, C.

-Notation "n ++ m" := (plus n m).
+Notation "n ++ m" := (plus n m).

-Notation "n ++ m" := (mult n m). +Notation "n ++ m" := (mult n m).
-Notation "n ** m" := (plus n m) (at level 60).
+Notation "n ** m" := (plus n m) (at level 60).

-Notation "n ▵ m" := (plus n m) (at level 60).
+Notation "n ▵ m" := (plus n m) (at level 60).

-Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).
+Notation "n '_' ++ 'x' m" := (plus n m) (at level 3).

-Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A
+Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A

-where "x = y :> A" := (@eq A x y) : type_scope.
+where "x = y :> A" := (@eq A x y) : type_scope.

-Definition eq0 := 0 = 0 :> nat.
+Definition eq0 := 0 = 0 :> nat.

-Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).
+Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).

-Definition b_α := ((0#0;0) , (0 ** 0)).
+Definition b_α := ((0#0;0) , (0 ** 0)).

Notation h := a.
@@ -97,7 +97,7 @@ Various checks for coqdoc     Variables b' b2: nat.

-    Notation "n + m" := (n ▵ m) : my_scope.
+    Notation "n + m" := (n ▵ m) : my_scope.

    Delimit Scope my_scope with my.
@@ -106,19 +106,19 @@ Various checks for coqdoc     Notation l := 0.

-    Definition α := (0 + l)%my.
+    Definition α := (0 + l)%my.

-    Definition a' b := b'++0++b2 _ ++x b.
+    Definition a' b := b'++0++b2 _ ++x b.

-    Definition c := {True}+{True}.
+    Definition c := {True}+{True}.

-    Definition d := (1+2)%nat.
+    Definition d := (1+2)%nat.

-    Lemma e : nat + nat.
+    Lemma e : nat + nat.
    Admitted.

@@ -137,7 +137,7 @@ Various checks for coqdoc       Variables b2: nat.

-      Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.
+      Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.

    End test.
-- cgit v1.2.3