From 261103b5bfd89335d028bf800af3f0a1ab1b70e5 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 9 Mar 2010 15:13:00 +0000
Subject: New HTML documentation generator

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1286 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 doc/removeproofs.mll | 35 -----------------------------------
 1 file changed, 35 deletions(-)
 delete mode 100644 doc/removeproofs.mll

(limited to 'doc/removeproofs.mll')

diff --git a/doc/removeproofs.mll b/doc/removeproofs.mll
deleted file mode 100644
index 7fb37bb0..00000000
--- 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
-}
-
-- 
cgit