1 files changed, 0 insertions, 105 deletions
diff --git a/doc/tradv8.ml4 b/doc/tradv8.ml4
deleted file mode 100644
index f050f7537..000000000
--- a/doc/tradv8.ml4
+++ /dev/null
@@ -1,105 +0,0 @@
-
-open Printf
-
-let file = Sys.argv.(1)
-
-let cin = open_in file
-let cout = open_out (file ^ ".v8")
-
-let (coq_out, coq_in) as chan = Unix.open_process "coqtop -translate"
-
-let begin_coq = 
-  Str.regexp 
-    "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$"
-
-let end_coq = 
-  Str.regexp 
-    "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\|eval\\)}[ \t]*$"
-
-let new_syntax =
-  Str.regexp "New Syntax:[ \t]*$"
-
-(* on envoie un Check O et on saute les 2 premiers New Syntax *)
-let _ =
-  output_string coq_in "Check O.\n";
-  flush coq_in;
-  while not (Str.string_match new_syntax (input_line coq_out) 0) do () done;
-  while not (Str.string_match new_syntax (input_line coq_out) 0) do () done;
-  printf "** init terminée\n"; flush stdout
-
-let iter_char_until_dot cin f =
-  printf "** entrée dans iter_char\n"; flush stdout;
-  let last_c = ref ' ' in
-  let rec loop () =
-    let c = input_char cin in
-    printf "[%c]" c; flush stdout;
-    f c;
-    if !last_c = '.' && (c = ' ' || c = '\t' || c = '\n') then 
-      () 
-    else begin
-      last_c := c;
-      loop ()
-    end
-  in
-  loop ()
-    
-let trad_commands () =
-  (* on copie toutes les commandes dans un fichier temporaire *)
-  let tmp = Filename.temp_file "trad" ".v" in
-  let tmp_in, end_s = 
-    let tmp_out = open_out tmp in
-    let rec loop () =
-      let s = input_line cin in
-      if Str.string_match end_coq s 0 then begin
-	close_out tmp_out;
-	open_in tmp, s
-      end else begin
-	output_string tmp_out (s ^ "\n");
-	loop ()
-      end
-    in
-    loop ()
-  in
-  ignore (Sys.command (Printf.sprintf "cat %s" tmp));
-  let one_command () =
-    (* on envoie toute la commande a Coq *)
-    iter_char_until_dot tmp_in (fun c -> output_char coq_in c);
-    (* on flush *)
-    flush coq_in;
-    (* on lit la réponse *)
-    try
-      (* 1. on cherche la ligne "New Syntax:" *)
-      while true do 
-	let s = input_line coq_out in
-	if Str.string_match new_syntax s 0 then raise Exit
-      done
-    with Exit ->
-      (* 2. on copie tout jusqu'au point *)
-      printf "** New Syntax trouvé\n"; flush stdout;
-      iter_char_until_dot coq_out (fun c -> output_char cout c);
-      printf "** copie terminée\n"; flush stdout;
-      flush cout
-  in    
-  try
-    while true do one_command () done; assert false
-  with End_of_file ->
-    printf "** End_of_file\n"; flush stdout;
-    Sys.remove tmp;
-    end_s
-
-let trad () =
-  while true do
-    let s = input_line cin in
-    output_string cout (s ^ "\n");
-    if Str.string_match begin_coq s 0 then 
-      let s = trad_commands () in
-      output_string cout (s ^ "\n");
-  done
-
-let _ =
-  try 
-    trad () 
-  with End_of_file -> 
-    close_out cout; 
-    printf "** close_out cout\n"; flush stdout;
-    ignore (Unix.close_process chan)