summaryrefslogtreecommitdiff
path: root/doc/removeproofs.mll
diff options
context:
space:
mode:
Diffstat (limited to 'doc/removeproofs.mll')
-rw-r--r--doc/removeproofs.mll35
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
-}
-