From 8506a4d60417ce498ce4525de044a6a590a5e922 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 29 Jul 2015 18:38:27 +0200
Subject: Rewrite the main loop of coq-tex.

Before this commit, coq-tex was reading the .v file and was guessing how
many lines from the coqtop output it should display. Now, it reads the
coqtop output and it guesses how many lines from the .v file it should
display. That way, coq-tex no longer needs to embed a parser; it relies
on coqtop for parsing.

This is much more robust and makes it possible to properly handle script
such as the following one:

  Goal { True }
     + { False }.
  { left. exact I. }

As before, if there is a way for a script to produce something that looks
like a prompt (that is, a line that starts with "foo < "), coq-tex will be
badly confused.
---
 tools/coq_tex.ml | 160 ++++++++++++++++++++++++++-----------------------------
 1 file changed, 76 insertions(+), 84 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index fc652f584..9a5ff86ef 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -24,10 +24,7 @@ let hrule = ref false
 let small = ref false
 let boot = ref false
 
-let coq_prompt = Str.regexp "Coq < "
-let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
-
-let remove_prompt s = Str.replace_first any_prompt "" s
+let any_prompt = Str.regexp "[A-Z0-9a-z_\\$']* < "
 
 (* First pass: extract the Coq phrases to evaluate from [texfile]
  * and put them into the file [inputv] *)
@@ -66,9 +63,6 @@ let extract texfile inputv =
 let begin_coq_example =
   Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
 let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
-let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
-let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
-let dot_end_line = Str.regexp "\\(\\.\\|}\\)[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
 
 let has_match r s =
   try let _ = Str.search_forward r s 0 in true with Not_found -> false
@@ -111,99 +105,97 @@ let insert texfile coq_output result =
   let c_tex = open_in texfile in
   let c_coq = open_in coq_output in
   let c_out = open_out result in
-  (* next_block k : this function reads the next block of Coq output
-   * removing the k leading prompts.
-   * it returns the block as a list of string) *)
-  let last_read = ref "" in
-  let next_block k =
-    if !last_read = "" then last_read := input_line c_coq;
-    (* skip k prompts *)
-    for _i = 1 to k do
-      last_read := remove_prompt !last_read;
-    done;
+  (* read lines until a prompt is found (starting from the second line),
+     purge prompts on the first line and return their number *)
+  let last_read = ref (input_line c_coq) in
+  let read_output () =
+    let first = !last_read in
+    let nb = ref 0 in
+    (* remove the leading prompts *)
+    let rec skip_prompts pos =
+      if Str.string_match any_prompt first pos then
+        let () = incr nb in
+        skip_prompts (Str.match_end ())
+      else pos in
+    let first =
+      let start = skip_prompts 0 in
+      String.sub first start (String.length first - start) in
     (* read and return the following lines until a prompt is found *)
     let rec read_lines () =
       let s = input_line c_coq in
       if Str.string_match any_prompt s 0 then begin
 	last_read := s; []
       end else
-	s :: (read_lines ())
-    in
-    let first = !last_read in first :: (read_lines ())
-  in
-  (* we are just after \end{coq_...} block *)
-  let rec just_after () =
+	s :: read_lines () in
+    (first :: read_lines (), !nb) in
+  let unhandled_output = ref None in
+  (* we are inside a \begin{coq_...} ... \end{coq_...} block
+   * show_... tell what kind of block it is *)
+  let rec inside show_answers show_questions not_first =
     let s = input_line c_tex in
-    if Str.string_match begin_coq_example s 0 then begin
-      inside (Str.matched_group 1 s <> "example*")
-             (Str.matched_group 1 s <> "example#") 0 false
-    end
-    else begin
-      if !hrule then output_string c_out "\\hrulefill\\\\\n";
-      output_string c_out "\\end{flushleft}\n";
-      if !small then output_string c_out "\\end{small}\n";
-      if Str.string_match begin_coq_eval s 0 then
-	eval 0
+    if not (Str.string_match end_coq s 0) then begin
+      let (bl,n) =
+        match !unhandled_output with
+        | Some some -> unhandled_output := None; some
+        | None -> read_output () in
+      assert (n > 0);
+      if not_first then output_string c_out "\\medskip\n";
+      if !verbose then Printf.printf "Coq < %s\n" s;
+      if show_questions then encapsule false c_out ("Coq < " ^ s);
+      let rec read_lines k =
+        if k = 0 then []
+        else
+          let s = input_line c_tex in
+          if Str.string_match end_coq s 0 then []
+          else s :: read_lines (k - 1) in
+      let al = read_lines (n - 1) in
+      if !verbose then List.iter (Printf.printf "      %s\n") al;
+      if show_questions then
+        List.iter (fun s -> encapsule false c_out ("      " ^ s)) al;
+      let la = n - 1 - List.length al in
+      if la <> 0 then
+        (* this happens when the block ends with a comment; the output
+           is for the command at the beginning of the next block *)
+        unhandled_output := Some (bl, la)
       else begin
-	output_string c_out (s ^ "\n");
-	outside ()
+        if !verbose then List.iter print_endline bl;
+        if show_answers then print_block c_out bl;
+        inside show_answers show_questions (show_answers || show_questions)
       end
-    end
+    end in
   (* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
-  and outside () =
-    let s = input_line c_tex in
-    if Str.string_match begin_coq_example s 0 then begin
+  let rec outside just_after =
+    let start_block () =
       if !small then output_string c_out "\\begin{small}\n";
       output_string c_out "\\begin{flushleft}\n";
+      if !hrule then output_string c_out "\\hrulefill\\\\\n" in
+    let end_block () =
       if !hrule then output_string c_out "\\hrulefill\\\\\n";
-      inside (Str.matched_group 1 s <> "example*")
-             (Str.matched_group 1 s <> "example#") 0 true
-    end else if Str.string_match begin_coq_eval s 0 then
-      eval 0
-    else begin
-      output_string c_out (s ^ "\n");
-      outside ()
-    end
-  (* we are inside a \begin{coq_example?} ... \end{coq_example?} block
-   * show_answers tells what kind of block it is
-   * k is the number of lines read until now *)
-  and inside show_answers  show_questions k first_block =
+      output_string c_out "\\end{flushleft}\n";
+      if !small then output_string c_out "\\end{small}\n" in
     let s = input_line c_tex in
-    if Str.string_match end_coq_example s 0 then begin
-      just_after ()
+    if Str.string_match begin_coq s 0 then begin
+      let kind = Str.matched_group 1 s in
+      if kind = "eval" then begin
+        if just_after then end_block ();
+        inside false false false;
+        outside false
+      end else begin
+        let show_answers   = kind <> "example*" in
+        let show_questions = kind <> "example#" in
+        if not just_after then start_block ();
+        inside show_answers show_questions just_after;
+        outside true
+      end
     end else begin
-      let prompt = if k = 0 then "Coq < " else "      " in
-      if !verbose then Printf.printf "%s%s\n" prompt s;
-      if (not first_block) && k=0 then output_string c_out "\\medskip\n";
-      if show_questions then encapsule false c_out (prompt ^ s);
-      if has_match dot_end_line s then begin
-	let bl = next_block (succ k) in
-	if !verbose then List.iter print_endline bl;
-	if show_answers then print_block c_out bl;
-	inside show_answers  show_questions 0 false
-      end else
-	inside show_answers  show_questions (succ k) first_block
-    end
-  (* we are inside a \begin{coq_eval} ... \end{coq_eval} block
-   * k is the number of lines read until now *)
-  and eval k =
-    let s = input_line c_tex in
-    if Str.string_match end_coq_eval s 0 then
-      outside ()
-    else begin
-      if !verbose then Printf.printf "Coq < %s\n" s;
-      if has_match dot_end_line s then
-	let bl = next_block (succ k) in
-	if !verbose then List.iter print_endline bl;
-	eval 0
-      else
-	eval (succ k)
-    end
-  in
+      if just_after then end_block ();
+      output_string c_out (s ^ "\n");
+      outside false
+    end in
   try
-    let _ = next_block 0 in (* to skip the Coq banner *)
-    let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *)
-    outside ()
+    let _ = read_output () in (* to skip the Coq banner *)
+    let _ = read_output () in (* to skip the Coq answer to Set Printing Width *)
+    outside false
   with End_of_file -> begin
     close_in c_tex;
     close_in c_coq;
-- 
cgit v1.2.3


From ffb2788b92323901c1024d1eae221e4beb4b6670 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 29 Jul 2015 19:07:54 +0200
Subject: Remove empty commands from the output of coq-tex.

---
 tools/coq_tex.ml | 29 +++++++++++++++++++----------
 1 file changed, 19 insertions(+), 10 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 9a5ff86ef..9c91889a0 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -129,16 +129,20 @@ let insert texfile coq_output result =
 	s :: read_lines () in
     (first :: read_lines (), !nb) in
   let unhandled_output = ref None in
+  let read_output () =
+    match !unhandled_output with
+    | Some some -> unhandled_output := None; some
+    | None -> read_output () in
   (* we are inside a \begin{coq_...} ... \end{coq_...} block
    * show_... tell what kind of block it is *)
-  let rec inside show_answers show_questions not_first =
+  let rec inside show_answers show_questions not_first discarded =
     let s = input_line c_tex in
-    if not (Str.string_match end_coq s 0) then begin
-      let (bl,n) =
-        match !unhandled_output with
-        | Some some -> unhandled_output := None; some
-        | None -> read_output () in
-      assert (n > 0);
+    if s = "" then
+      inside show_answers show_questions not_first (discarded + 1)
+    else if not (Str.string_match end_coq s 0) then begin
+      let (bl,n) = read_output () in
+      assert (n > discarded);
+      let n = n - discarded in
       if not_first then output_string c_out "\\medskip\n";
       if !verbose then Printf.printf "Coq < %s\n" s;
       if show_questions then encapsule false c_out ("Coq < " ^ s);
@@ -160,8 +164,13 @@ let insert texfile coq_output result =
       else begin
         if !verbose then List.iter print_endline bl;
         if show_answers then print_block c_out bl;
-        inside show_answers show_questions (show_answers || show_questions)
+        inside show_answers show_questions (show_answers || show_questions) 0
       end
+    end else if discarded > 0 then begin
+      (* this happens when the block ends with an empty line *)
+      let (bl,n) = read_output () in
+      assert (n > discarded);
+      unhandled_output := Some (bl, n - discarded)
     end in
   (* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
   let rec outside just_after =
@@ -178,13 +187,13 @@ let insert texfile coq_output result =
       let kind = Str.matched_group 1 s in
       if kind = "eval" then begin
         if just_after then end_block ();
-        inside false false false;
+        inside false false false 0;
         outside false
       end else begin
         let show_answers   = kind <> "example*" in
         let show_questions = kind <> "example#" in
         if not just_after then start_block ();
-        inside show_answers show_questions just_after;
+        inside show_answers show_questions just_after 0;
         outside true
       end
     end else begin
-- 
cgit v1.2.3


From 9a5fb78ef3c7c5d4f568a4d04e169475e9105def Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 29 Jul 2015 19:58:39 +0200
Subject: Make coq-tex more robust with respect to the (non-)command on the
 last line.

---
 tools/coq_tex.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 9c91889a0..f65708698 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -55,7 +55,10 @@ let extract texfile inputv =
       ("Set Printing Width " ^ (string_of_int !linelen) ^".\n");
     outside ()
   with End_of_file ->
-    begin close_in chan_in; close_out chan_out end
+    (* a dummy command, just in case the last line was a comment *)
+    output_string chan_out "Set Printing Width 78.\n";
+    close_in chan_in;
+    close_out chan_out
 
 (* Second pass: insert the answers of Coq from [coq_output] into the
  * TeX file [texfile]. The result goes in file [result]. *)
-- 
cgit v1.2.3


From 5383cdc276d9ba7f1bb05bfe5aeae0a25edbd4a4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 30 Jul 2015 07:56:49 +0200
Subject: Remove usage of Printexc.catch in the tools, as it is deprecated
 since 2001.

"This function is deprecated: the runtime system is now able to print
uncaught exceptions as precisely as Printexc.catch does. Moreover, calling
Printexc.catch makes it harder to track the location of the exception
using the debugger or the stack backtrace facility. So, do not use
Printexc.catch in new code."
---
 tools/coq_makefile.ml | 4 +---
 tools/coq_tex.ml      | 4 +---
 tools/coqdep_boot.ml  | 4 +---
 tools/coqdoc/main.ml  | 4 +---
 tools/coqwc.mll       | 4 +---
 tools/gallina.ml      | 5 +----
 6 files changed, 6 insertions(+), 19 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 8f4772e28..71134c2d9 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -842,11 +842,9 @@ let do_makefile args =
   if not (makefile = None) then close_out !output_channel;
   exit 0
 
-let main () =
+let _ =
   let args =
     if Array.length Sys.argv = 1 then usage ();
     List.tl (Array.to_list Sys.argv)
   in
     do_makefile args
-
-let _ = Printexc.catch main ()
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index f65708698..53444cee7 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -285,7 +285,7 @@ let find_coqtop () =
     "coqtop"
   end
 
-let main () =
+let _ =
   parse_cl ();
   if !image = "" then image := Filename.quote (find_coqtop ());
   if !boot then image := !image ^ " -boot";
@@ -298,5 +298,3 @@ let main () =
     flush stdout
   end;
   List.iter one_file (List.rev !files)
-
-let _ = Printexc.catch main ()
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index 2d5fd36a6..64ce66d2d 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -30,7 +30,7 @@ let rec parse = function
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
-let coqdep_boot () =
+let _ =
   let () = option_boot := true in
   if Array.length Sys.argv < 2 then exit 1;
   parse (List.tl (Array.to_list Sys.argv));
@@ -47,5 +47,3 @@ let coqdep_boot () =
   end;
   if !option_c then mL_dependencies ();
   coq_dependencies ()
-
-let _ = Printexc.catch coqdep_boot ()
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 9531cd2b0..2554ed495 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -557,10 +557,8 @@ let produce_output fl =
 (*s \textbf{Main program.} Print the banner, parse the command line,
     read the files and then call [produce_document] from module [Web]. *)
 
-let main () =
+let _ =
   let files = parse () in
     Index.init_coqlib_library ();
     if not !quiet then banner ();
     if files <> [] then produce_output files
-
-let _ = Printexc.catch main ()
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 417ec5355..9a42553da 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -276,7 +276,7 @@ let rec parse = function
 
 (*s Main program. *)
 
-let main () =
+let _ =
   let files = parse (List.tl (Array.to_list Sys.argv)) in
   if not (!spec_only || !proof_only) then
     printf "     spec    proof comments\n";
@@ -285,8 +285,6 @@ let main () =
     | [f] -> process_file f
     | _ -> List.iter process_file files; print_totals ()
 
-let _ = Printexc.catch main ()
-
 (*i*)}(*i*)
 
 
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 279919c58..5ce19e7f8 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -39,7 +39,7 @@ let traite_stdin () =
   with Sys_error _ ->
     ()
 
-let gallina () =
+let _ =
   let lg_command = Array.length Sys.argv in
   if lg_command < 2 then begin
     output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n";
@@ -59,6 +59,3 @@ let gallina () =
     traite_stdin ()
   else
     List.iter traite_fichier !vfiles
-
-let _ = Printexc.catch gallina ()
-
-- 
cgit v1.2.3


From 52940b19a7f47fa5022d75c5679785ac90aaa0dc Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 30 Jul 2015 08:10:05 +0200
Subject: Remove unused variables.

---
 tools/coq_tex.ml | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 53444cee7..26a9715ef 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -63,17 +63,6 @@ let extract texfile inputv =
 (* Second pass: insert the answers of Coq from [coq_output] into the
  * TeX file [texfile]. The result goes in file [result]. *)
 
-let begin_coq_example =
-  Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
-let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
-
-let has_match r s =
-  try let _ = Str.search_forward r s 0 in true with Not_found -> false
-
-let percent = Str.regexp "%"
-let bang    = Str.regexp "!"
-let expos   = Str.regexp "^"
-
 let tex_escaped s =
   let dollar = "\\$" and  backslash = "\\\\" and expon = "\\^" in
   let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in
@@ -216,7 +205,7 @@ let insert texfile coq_output result =
 
 (* Process of one TeX file *)
 
-let rm f = try Sys.remove f with any -> ()
+let rm f = try Sys.remove f with _ -> ()
 
 let one_file texfile =
   let inputv = Filename.temp_file "coq_tex" ".v" in
-- 
cgit v1.2.3


From 070139d3a82ea23e4d050dd5ccebe3f17047cc62 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 30 Jul 2015 08:19:10 +0200
Subject: Fix broken regexp.

Characters do not need to be escaped in character ranges. It just had the
effect of matching backslashes four times.
---
 tools/coq_tex.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 26a9715ef..8218f84f1 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -64,8 +64,7 @@ let extract texfile inputv =
  * TeX file [texfile]. The result goes in file [result]. *)
 
 let tex_escaped s =
-  let dollar = "\\$" and  backslash = "\\\\" and expon = "\\^" in
-  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in
+  let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in
   let adapt_delim = function
     | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
     | "\\" -> "{\\char'134}"
-- 
cgit v1.2.3


From a9f3607ae72517156301570a4ffa05908609b7e0 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 30 Jul 2015 08:30:00 +0200
Subject: Fix width of underscore in coq_tex output.

---
 tools/coq_tex.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 8218f84f1..dbdc2e9db 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -66,7 +66,8 @@ let extract texfile inputv =
 let tex_escaped s =
   let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in
   let adapt_delim = function
-    | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "_" -> "{\\char`\\_}"
     | "\\" -> "{\\char'134}"
     | "^" -> "{\\char'136}"
     | "~" -> "{\\char'176}"
-- 
cgit v1.2.3


From 505eb0f0dae9b8a6ac810070d60916b67942b305 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Fri, 31 Jul 2015 09:34:48 +0200
Subject: Remove some outdated files and fix permissions.

---
 README.doc                                       |  0
 doc/common/macros.tex                            |  0
 doc/common/title.tex                             |  0
 doc/stdlib/Library.tex                           |  0
 doc/tutorial/Tutorial.tex                        |  0
 test-suite/interactive/ParalITP_smallproofs.v    |  0
 test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v |  0
 theories/Arith/intro.tex                         | 55 ------------------------
 theories/Bool/intro.tex                          | 16 -------
 theories/Lists/intro.tex                         | 20 ---------
 theories/Logic/intro.tex                         |  8 ----
 theories/NArith/intro.tex                        |  5 ---
 theories/PArith/intro.tex                        |  4 --
 theories/Reals/intro.tex                         |  4 --
 theories/Relations/intro.tex                     | 23 ----------
 theories/Setoids/intro.tex                       |  1 -
 theories/Sets/intro.tex                          | 24 -----------
 theories/Sorting/intro.tex                       |  1 -
 theories/Wellfounded/intro.tex                   |  4 --
 theories/ZArith/intro.tex                        |  6 ---
 tools/README.coq-tex                             | 13 ------
 tools/README.emacs                               |  0
 tools/coq-sl.sty                                 |  0
 23 files changed, 184 deletions(-)
 mode change 100755 => 100644 README.doc
 mode change 100755 => 100644 doc/common/macros.tex
 mode change 100755 => 100644 doc/common/title.tex
 mode change 100755 => 100644 doc/stdlib/Library.tex
 mode change 100755 => 100644 doc/tutorial/Tutorial.tex
 mode change 100755 => 100644 test-suite/interactive/ParalITP_smallproofs.v
 mode change 100755 => 100644 test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
 delete mode 100755 theories/Arith/intro.tex
 delete mode 100644 theories/Bool/intro.tex
 delete mode 100755 theories/Lists/intro.tex
 delete mode 100755 theories/Logic/intro.tex
 delete mode 100644 theories/NArith/intro.tex
 delete mode 100644 theories/PArith/intro.tex
 delete mode 100644 theories/Reals/intro.tex
 delete mode 100755 theories/Relations/intro.tex
 delete mode 100644 theories/Setoids/intro.tex
 delete mode 100755 theories/Sets/intro.tex
 delete mode 100644 theories/Sorting/intro.tex
 delete mode 100755 theories/Wellfounded/intro.tex
 delete mode 100755 theories/ZArith/intro.tex
 delete mode 100755 tools/README.coq-tex
 mode change 100755 => 100644 tools/README.emacs
 mode change 100755 => 100644 tools/coq-sl.sty

(limited to 'tools')

diff --git a/README.doc b/README.doc
old mode 100755
new mode 100644
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
old mode 100755
new mode 100644
diff --git a/doc/common/title.tex b/doc/common/title.tex
old mode 100755
new mode 100644
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex
old mode 100755
new mode 100644
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
old mode 100755
new mode 100644
diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v
old mode 100755
new mode 100644
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
old mode 100755
new mode 100644
diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex
deleted file mode 100755
index 655de34ca..000000000
--- a/theories/Arith/intro.tex
+++ /dev/null
@@ -1,55 +0,0 @@
-\section{Arith}\label{Arith}
-
-The {\tt Arith} library deals with various arithmetical notions and 
-their properties.
-
-\subsection*{Standard {\tt Arith} library}
-
-The following files are automatically loaded by {\tt Require Arith}.
-
-\begin{itemize}
-
-\item {\tt Le.v} states and proves properties of the large order {\tt le}.
-
-\item {\tt Lt.v} states and proves properties of the strict order {\tt 
-lt} (especially, the relationship with {\tt le}).
-
-\item {\tt Plus.v} states and proves properties on the addition.
-
-\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}.
-
-\item {\tt Minus.v} defines the difference on 
-{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is 
-{\tt O} if {\tt n} $<$ {\tt p}.
-
-\item {\tt Mult.v} states and proves properties on the multiplication.
-
-\item {\tt Between.v} defines modalities on {\tt nat} and proves properties 
-of them.
-
-\end{itemize}
-
-\subsection*{Additional {\tt Arith} library}
-
-\begin{itemize}
-
-\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state
-and prove various decidability results on {\tt nat}.
-
-\item {\tt Wf\_nat.v} states and proves various induction and recursion 
-principles on {\tt nat}. Especially, recursion for objects measurable by 
-a natural number and recursion on {\tt nat * nat} are provided.
-
-\item {\tt Min.v} defines the minimum of two natural numbers and proves 
-properties of it. 
-
-\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows 
-the equivalence with Leibniz' equality.
-
-\item {\tt Euclid.v} proves that the euclidean
-division specification is realisable. Conversely, {\tt Div.v} exhibits
-two different algorithms and semi-automatically reconstruct the proof of
-their correctness. These files emphasize the extraction of program vs
-reconstruction of proofs paradigm.
-
-\end{itemize}
diff --git a/theories/Bool/intro.tex b/theories/Bool/intro.tex
deleted file mode 100644
index 22ee38aab..000000000
--- a/theories/Bool/intro.tex
+++ /dev/null
@@ -1,16 +0,0 @@
-\section{Bool}\label{Bool}
-
-The BOOL library includes the following files:
-
-\begin{itemize}
-
-\item {\tt Bool.v} defines standard operations on booleans and states
-  and proves simple facts on them.
-\item {\tt IfProp.v} defines a disjunction which contains its proof
-  and states its properties.
-\item {\tt Zerob.v} defines the test against 0 on natural numbers and
-  states and proves properties of it.
-\item {\tt Orb.v} states and proves facts on the boolean or.
-\item {\tt DecBool.v} defines a conditional from a proof of
-  decidability and states its properties.
-\end{itemize}
diff --git a/theories/Lists/intro.tex b/theories/Lists/intro.tex
deleted file mode 100755
index d372de8ed..000000000
--- a/theories/Lists/intro.tex
+++ /dev/null
@@ -1,20 +0,0 @@
-\section{Lists}\label{Lists}
-
-This library includes the following files:
-
-\begin{itemize}
-
-\item {\tt List.v} contains definitions of (polymorphic) lists, 
-  functions on lists such as head, tail, map, append and prove some
-  properties of these functions. Implicit arguments are used in this
-  library, so you should read the Reference Manual about implicit
-  arguments before using it.
-
-\item {\tt ListSet.v} contains definitions and properties of finite
-  sets, implemented as lists.
-
-\item {\tt Streams.v} defines the type of infinite lists (streams). It is a
-  co-inductive type. Basic facts are stated and proved. The streams are
-  also polymorphic.
-
-\end{itemize}
diff --git a/theories/Logic/intro.tex b/theories/Logic/intro.tex
deleted file mode 100755
index 1fb294f2f..000000000
--- a/theories/Logic/intro.tex
+++ /dev/null
@@ -1,8 +0,0 @@
-\section{Logic}\label{Logic}
-
-This library deals with classical logic and its properties.
-The main file is {\tt Classical.v}.
-
-This library also provides some facts on equalities for dependent
-types. See the files {\tt Eqdep.v} and {\tt JMeq.v}.
-
diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex
deleted file mode 100644
index bf39bc36c..000000000
--- a/theories/NArith/intro.tex
+++ /dev/null
@@ -1,5 +0,0 @@
-\section{Binary natural numbers : NArith}\label{NArith}
-
-Here are defined various arithmetical notions and their properties,
-similar to those of {\tt Arith}.
-
diff --git a/theories/PArith/intro.tex b/theories/PArith/intro.tex
deleted file mode 100644
index ffce881ed..000000000
--- a/theories/PArith/intro.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-\section{Binary positive integers : PArith}\label{PArith}
-
-Here are defined various arithmetical notions and their properties,
-similar to those of {\tt Arith}.
diff --git a/theories/Reals/intro.tex b/theories/Reals/intro.tex
deleted file mode 100644
index 433172585..000000000
--- a/theories/Reals/intro.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-\section{Reals}\label{Reals}
-
-This library contains an axiomatization of real numbers.
-The main file is \texttt{Reals.v}.
diff --git a/theories/Relations/intro.tex b/theories/Relations/intro.tex
deleted file mode 100755
index 5056f36f9..000000000
--- a/theories/Relations/intro.tex
+++ /dev/null
@@ -1,23 +0,0 @@
-\section{Relations}\label{Relations}
-
-This library develops closure properties of relations.
-
-\begin{itemize}
-\item {\tt Relation\_Definitions.v} deals with the general notions
-  about binary relations (orders, equivalences, ...)
-
-\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various
-  closures of relations (by symmetry, by transitivity, ...) and
-  lexicographic orderings.
-
-\item {\tt Operators\_Properties.v} states and proves facts on the
-  various closures of a relation.
-
-\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt
-    Relation\_Operators.v} and \\
-    {\tt Operators\_Properties.v} together.
-
-\item {\tt Newman.v} proves Newman's lemma on noetherian and locally
-  confluent relations.
-
-\end{itemize}
diff --git a/theories/Setoids/intro.tex b/theories/Setoids/intro.tex
deleted file mode 100644
index 50cd025de..000000000
--- a/theories/Setoids/intro.tex
+++ /dev/null
@@ -1 +0,0 @@
-\section{Setoids}\label{Setoids}
diff --git a/theories/Sets/intro.tex b/theories/Sets/intro.tex
deleted file mode 100755
index 83c2177fd..000000000
--- a/theories/Sets/intro.tex
+++ /dev/null
@@ -1,24 +0,0 @@
-\section{Sets}\label{Sets}
-
-This is a library on sets defined by their characteristic predicate.
-It contains the following modules:
-
-\begin{itemize}
-\item {\tt Ensembles.v}
-\item {\tt Constructive\_sets.v}, {\tt Classical\_sets.v}
-\item {\tt Relations\_1.v}, {\tt Relations\_2.v}, 
- {\tt Relations\_3.v}, {\tt Relations\_1\_facts.v},  \\
- {\tt Relations\_2\_facts.v}, {\tt Relations\_3\_facts.v}
-\item {\tt Partial\_Order.v}, {\tt Cpo.v}
-\item {\tt Powerset.v}, {\tt Powerset\_facts.v}, 
- {\tt Powerset\_Classical\_facts.v}
-\item {\tt Finite\_sets.v}, {\tt Finite\_sets\_facts.v}
-\item {\tt Image.v}
-\item {\tt Infinite\_sets.v}
-\item {\tt Integers.v}
-\end{itemize}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
diff --git a/theories/Sorting/intro.tex b/theories/Sorting/intro.tex
deleted file mode 100644
index 64ae4c888..000000000
--- a/theories/Sorting/intro.tex
+++ /dev/null
@@ -1 +0,0 @@
-\section{Sorting}\label{Sorting}
diff --git a/theories/Wellfounded/intro.tex b/theories/Wellfounded/intro.tex
deleted file mode 100755
index 126071e28..000000000
--- a/theories/Wellfounded/intro.tex
+++ /dev/null
@@ -1,4 +0,0 @@
-\section{Well-founded relations}\label{Wellfounded}
-
-This library gives definitions and results about well-founded relations.
-
diff --git a/theories/ZArith/intro.tex b/theories/ZArith/intro.tex
deleted file mode 100755
index 21e52c198..000000000
--- a/theories/ZArith/intro.tex
+++ /dev/null
@@ -1,6 +0,0 @@
-\section{Binary integers : ZArith}
-The {\tt ZArith} library deals with binary integers (those used
-by the {\tt Omega} decision tactic).
-Here are defined various arithmetical notions and their properties,
-similar to those of {\tt Arith}.
-
diff --git a/tools/README.coq-tex b/tools/README.coq-tex
deleted file mode 100755
index 5c7606a96..000000000
--- a/tools/README.coq-tex
+++ /dev/null
@@ -1,13 +0,0 @@
-DESCRIPTION.
-
-The coq-tex filter extracts Coq phrases embedded in LaTeX files,
-evaluates them, and insert the outcome of the evaluation after each
-phrase.
-
-The filter is written in Perl, so you'll need Perl version 4 installed
-on your machine.
-
-USAGE. See the manual page (coq-tex.1).
-
-AUTHOR. Jean-Christophe Filliatre (jcfillia@lip.ens-lyon.fr)
-  from caml-tex of Xavier Leroy.
diff --git a/tools/README.emacs b/tools/README.emacs
old mode 100755
new mode 100644
diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty
old mode 100755
new mode 100644
-- 
cgit v1.2.3