summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-05-26 11:57:57 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2010-05-26 11:57:57 +0000
commitee8556f646ac19726f012fff78fffdee39f5be63 (patch)
tree3b4f0e7fd5c8aaddf7bddd41142af982d56a4508 /doc
parentefc0f520d536e013740d34e40b298039fca40d19 (diff)
Clean up
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1348 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'doc')
-rw-r--r--doc/coq2html.mll25
1 files changed, 0 insertions, 25 deletions
diff --git a/doc/coq2html.mll b/doc/coq2html.mll
index dd7d3a9..566e066 100644
--- a/doc/coq2html.mll
+++ b/doc/coq2html.mll
@@ -45,31 +45,6 @@ let add_definition curmod pos sp id ty =
if not (Hashtbl.mem xref_table (curmod, pos))
then Hashtbl.add xref_table (curmod, pos) (Def(path sp id, ty))
-(*
-let read_glob_file f =
- let ic = open_in f in
- let curmod = ref "" in
- try
- while true do
- let s = input_line ic in
- try
- Scanf.sscanf s "F%s"
- (fun m -> curmod := m; add_module m)
- with Scanf.Scan_failure _ ->
- try
- Scanf.sscanf s "R%d %s %s %s %s"
- (fun pos dp sp id ty -> add_reference !curmod pos dp sp id ty)
- with Scanf.Scan_failure _ ->
- try
- Scanf.sscanf s "%s %d %s %s"
- (fun ty pos sp id -> add_definition !curmod pos sp id ty)
- with Scanf.Scan_failure _ ->
- ()
- done
- with End_of_file ->
- close_in ic
-*)
-
type link = Link of string | Anchor of string | Nolink
let coqlib_url = "http://coq.inria.fr/library/"