From a4a492ca1c1fe2caa3f5de785fe08662d9520725 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 29 Mar 2010 21:48:43 +0000
Subject: 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
---
 plugins/subtac/subtac_obligations.ml  | 2 +-
 plugins/subtac/subtac_obligations.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 24c5a1266d..1424618f00 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -49,7 +49,7 @@ type fixpoint_kind =
   | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
   | IsCoFixpoint
 
-type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
+type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
 
 type program_info = {
   prg_name: identifier;
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index aed5b58b7a..bc5fc3e100 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -30,7 +30,7 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
   ?reduce:(Term.constr -> Term.constr) ->
   ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress
 
-type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
+type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list
 
 type fixpoint_kind =
   | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
-- 
cgit v1.2.3