From e41be40fb1675311801f8c7f7039a44575a45fff Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 5 Apr 2020 16:47:01 +0200 Subject: Granting coqdoc wish #7093 (definitions link to themselves). Co-Authored-By: Xia Li-yao --- test-suite/coqdoc/binder.html.out | 2 +- test-suite/coqdoc/bug11194.html.out | 10 +++---- test-suite/coqdoc/bug11353.html.out | 10 +++---- test-suite/coqdoc/bug5648.html.out | 8 +++--- test-suite/coqdoc/bug5700.html.out | 4 +-- test-suite/coqdoc/links.html.out | 56 ++++++++++++++++++------------------- tools/coqdoc/output.ml | 3 +- 7 files changed, 47 insertions(+), 46 deletions(-) diff --git a/test-suite/coqdoc/binder.html.out b/test-suite/coqdoc/binder.html.out index a8ec7ae033..af8eb46845 100644 --- a/test-suite/coqdoc/binder.html.out +++ b/test-suite/coqdoc/binder.html.out @@ -27,7 +27,7 @@ Link binders

-Definition foo alpha beta := alpha + beta.
+Definition foo alpha beta := alpha + beta.
diff --git a/test-suite/coqdoc/bug11194.html.out b/test-suite/coqdoc/bug11194.html.out index 304d041033..6fc6533e59 100644 --- a/test-suite/coqdoc/bug11194.html.out +++ b/test-suite/coqdoc/bug11194.html.out @@ -19,11 +19,11 @@

Library Coqdoc.bug11194

-Record a_struct := { anum : nat }.
-Canonical Structure a_struct_0 := {| anum := 0|}.
-Definition rename_a_s_0 := a_struct_0.
-Coercion some_nat := (@Some nat).
-Definition rename_some_nat := some_nat.
+Record a_struct := { anum : nat }.
+Canonical Structure a_struct_0 := {| anum := 0|}.
+Definition rename_a_s_0 := a_struct_0.
+Coercion some_nat := (@Some nat).
+Definition rename_some_nat := some_nat.
diff --git a/test-suite/coqdoc/bug11353.html.out b/test-suite/coqdoc/bug11353.html.out index 7a1de45e6e..f9d6a79906 100644 --- a/test-suite/coqdoc/bug11353.html.out +++ b/test-suite/coqdoc/bug11353.html.out @@ -19,13 +19,13 @@

Library Coqdoc.bug11353

-Definition a := 0. #[ universes( template) ]
-Inductive mysum (A B:Type) : Type :=
-  | myinl : A → mysum A B
-  | myinr : B → mysum A B.
+Definition a := 0. #[ universes( template) ]
+Inductive mysum (A B:Type) : Type :=
+  | myinl : A → mysum A B
+  | myinr : B → mysum A B.

-#[local]Definition b := 1.
+#[local]Definition b := 1.
diff --git a/test-suite/coqdoc/bug5648.html.out b/test-suite/coqdoc/bug5648.html.out index 8201cd3ccb..e1d1c1313e 100644 --- a/test-suite/coqdoc/bug5648.html.out +++ b/test-suite/coqdoc/bug5648.html.out @@ -19,17 +19,17 @@

Library Coqdoc.bug5648

-Lemma a : True.
+Lemma a : True.
Proof.
auto.
Qed.

-Variant t :=
-| A | Add | G | Goal | L | Lemma | P | Proof .
+Variant t :=
+| A | Add | G | Goal | L | Lemma | P | Proof .

-Definition d x :=
+Definition d x :=
  match x with
  | A ⇒ 0
  | Add ⇒ 1
diff --git a/test-suite/coqdoc/bug5700.html.out b/test-suite/coqdoc/bug5700.html.out index b96fc6281d..286e8bba4d 100644 --- a/test-suite/coqdoc/bug5700.html.out +++ b/test-suite/coqdoc/bug5700.html.out @@ -26,7 +26,7 @@
-Definition const1 := 1.
+Definition const1 := 1.

@@ -36,7 +36,7 @@
-Definition const2 := 2.
+Definition const2 := 2.
diff --git a/test-suite/coqdoc/links.html.out b/test-suite/coqdoc/links.html.out index 3ec5e7eb23..12d284dc54 100644 --- a/test-suite/coqdoc/links.html.out +++ b/test-suite/coqdoc/links.html.out @@ -51,93 +51,93 @@ Various checks for coqdoc Require Import String.

-Definition g := "dfjkh""sdfhj forall <> * ~"%string.
+Definition g := "dfjkh""sdfhj forall <> * ~"%string.

-Definition a (b: nat) := b.
+Definition a (b: nat) := b.

-Definition f := ∀ C:Prop, C.
+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.
+Notation h := a.

-  Section test.
+  Section test.

-    Variables b' b2: nat.
+    Variables b' b2: nat.

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

    Delimit Scope my_scope with my.

-    Notation l := 0.
+    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.

  End test.

-  Section test2.
+  Section test2.

-    Variables b': nat.
+    Variables b': nat.

-    Section test.
+    Section test.

-      Variables b2: nat.
+      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.
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 04725aa26f..d6f51d7b78 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -659,7 +659,8 @@ module Html = struct let reference s r = match r with | Def (fullid,ty) -> - printf "" (sanitize_name fullid); + let s' = sanitize_name fullid in + printf "" s' s'; printf "%s" (type_name ty) s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s -- cgit v1.2.3