New HTML documentation generator

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 0 insertions, 35 deletions

diff --git a/doc/removeproofs.mll b/doc/removeproofs.mll
deleted file mode 100644
index 7fb37bb..0000000
--- a/doc/removeproofs.mll
+++ /dev/null
@@ -1,35 +0,0 @@
-rule process inproof oc = parse
-  | "<span class=\"keyword\">Proof</span>" ' '* '.'
-      { process true oc lexbuf }
-  | "<span class=\"keyword\">" ("Qed" | "Defined") "</span>" ' '* '.'
-      { process false oc lexbuf }
-(*
-  | "<a class=\"idref\" href=\"" 
-    [^ '"'] + '#' '"' [^ '\n' '>']* '"' '"' '>'
-    ([^ '<' '\n']+ as ident)
-    "</a>"
-      { if not inproof then output_string oc ident;
-        process inproof oc lexbuf }
-*)
-  | _
-      { if not inproof then output_char oc (Lexing.lexeme_char lexbuf 0);
-        process inproof oc lexbuf }
-  | eof
-      { () }
-
-{
-
-let process_file name =
-  let ic = open_in name in
-  Sys.remove name;
-  let oc = open_out name in
-  process false oc (Lexing.from_channel ic);
-  close_out oc;
-  close_in ic
-
-let _ =
-  for i = 1 to Array.length Sys.argv - 1 do
-    process_file Sys.argv.(i)
-  done
-}
-