diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-29 21:48:43 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-29 21:48:43 +0000 |
commit | a4a492ca1c1fe2caa3f5de785fe08662d9520725 (patch) | |
tree | f38723f9251f49f5352d3b18ce10ea9263c1cdf6 /test-suite/coqdoc | |
parent | 8bc1219464471054cd5f683c33bfa7ddf76802f6 (diff) |
Several bug-fixes and improvements of coqdoc
- make links to section variables working (used qualified names for
disambiguation and fixed the place in intern_var where to dump them)
(wish #2277)
- mapping of physical to logical paths now follows coq (see bug #2274)
(incidentally, it was also incorrectly seeing foobar.v as a in directory foo)
- added links for notations
- added new category "other" for indexing entries not starting with latin letter
(e.g. notations or non-latin identifiers which was otherwise broken)
- protected non-notation strings (from String.v) from utf8 symbol interpretation
- incidentally quoted parseable _ in notations to avoid confusion with
placeholder in the "_ + _" form of notation
- improved several "Sys_error" error messages
- fixed old bug about second dot of ".." being interpreted as regular dot
- removed obsolete lexer in index.mll (and renamed index.mll to index.ml)
- added a test-suite file for testing various features of coqdoc
Things that still do not work:
- when a notation is redefined several times in the same scope, only
the link to the first definition works
- if chars and symbols are not separated in advance, idents
that immediately follow symbols are not detected
(e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations
Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
line per each proper location covered by the notation)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12890 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/coqdoc')
-rw-r--r-- | test-suite/coqdoc/links.v | 102 |
1 files changed, 102 insertions, 0 deletions
diff --git a/test-suite/coqdoc/links.v b/test-suite/coqdoc/links.v new file mode 100644 index 000000000..b09d64a9a --- /dev/null +++ b/test-suite/coqdoc/links.v @@ -0,0 +1,102 @@ +(** 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 +- spliting 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 := forall C:Prop, C. + +Notation "n ++ m" := (plus n m). + +Notation "n ++ m" := (mult n m). (* redefinition *) + +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 p := ((0#0;0) , (0 % 0)). + +Notation h := a. + + Section test. + + Variables b' b2: nat. + + Notation "n + m" := (plus 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 *) + +(** skip *) + +(** skip *) + +(** skip *) + +(** skip *) + +(** skip *) + +(** skip *) + +(** skip *) + +(** skip *) + +(** skip *) + +(** skip *) + +(** skip *) + +(** skip *) + |