+ +

Library Coqdoc.links

+ +

+Various checks for coqdoc + +

+ +

symbols should not be inlined in string g + +
links to both kinds of notations in a' should work to the right notation + +
with utf8 option, forall must be unicode + +
splitting between symbols and ident should be correct in a' and c + +
".." should be rendered correctly + +

+ +

+ +
+Require Import String.
+ +
+Definition g := "dfjkh""sdfhj forall <> * ~"%string.
+ +
+Definition a (b: nat) := b.
+ +
+Definition f := ∀ C:Prop, C.
+ +
+Notation "n ++ m" := (plus 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 '_' ++ 'x' m" := (plus n m) (at level 3).
+ +
+Inductive eq (A:Type) (x:A) : A → Prop := eq_refl : x = x :>A
+
+where "x = y :> A" := (@eq A x y) : type_scope.
+ +
+Definition eq0 := 0 = 0 :> nat.
+ +
+Notation "( x # y ; .. ; z )" := (pair .. (pair x y) .. z).
+ +
+Definition b_α := ((0#0;0) , (0 ** 0)).
+ +
+Notation h := a.
+ +
+  Section test.
+ +
+    Variables b' b2: nat.
+ +
+    Notation "n + m" := (n ▵ m) : my_scope.
+ +
+    Delimit Scope my_scope with my.
+ +
+    Notation l := 0.
+ +
+    Definition α := (0 + l)%my.
+ +
+    Definition a' b := b'++0++b2 _ ++x b.
+ +
+    Definition c := {True }+{True }.
+ +
+    Definition d := (1+2)%nat.
+ +
+    Lemma e : nat + nat.
+    Admitted.
+ +
+  End test.
+ +
+  Section test2.
+ +
+    Variables b': nat.
+ +
+    Section test.
+ +
+      Variables b2: nat.
+ +
+      Definition a'' b := b' ++ O ++ b2 _ ++ x b + h 0.
+ +
+    End test.
+ +
+  End test2.
+ +
+

+ +

+skip +

+ + skip +

+ +
+