Merge PR #12289: test-suite: fix bug causing unit tests to be skipped

Reviewed-by: herbelin

2 files changed, 14 insertions, 61 deletions

diff --git a/test-suite/unit-tests/ide/lex_tests.ml b/test-suite/unit-tests/ide/lex_tests.ml
deleted file mode 100644
index 3082acdf1f..0000000000
--- a/test-suite/unit-tests/ide/lex_tests.ml
+++ /dev/null
@@ -1,50 +0,0 @@
-open Utest
-
-let log_out_ch = open_log_out_ch __FILE__
-
-let lex s =
-  let n =
-    let last = String.length s - 1 in
-    if s.[last] = '.' then Some last else None in
-  let stop = ref None in
-  let f i _ = assert(!stop = None); stop := Some i in
-  begin try Coq_lex.delimit_sentences f s
-  with Coq_lex.Unterminated -> () end;
-  if n <> !stop then begin
-    let p_opt = function None -> "None" | Some i -> "Some " ^ string_of_int i in
-    Printf.fprintf log_out_ch "ERROR: %S\nEXPECTED: %s\nGOT: %s\n" s (p_opt n) (p_opt !stop)
-  end;
-  n = !stop
-
-let i2s i = "test at line: " ^ string_of_int i
-
-let tests = [
-
-  mk_bool_test (i2s __LINE__) "no quotation" @@ lex
-  "foo.+1 bar."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation" @@ lex
-  "foo constr:(xxx)."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot" @@ lex
-  "foo constr:(xxx. yyy)."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot double paren" @@ lex
-  "foo constr:((xxx. (foo.+1 ) \")\" yyy))."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot paren [" @@ lex
-  "foo constr:[xxx. (foo.+1 ) \")\" yyy]."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot double paren [" @@ lex
-  "foo constr:[[xxx. (foo.+1 ) \")\" yyy]]."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation with dot triple paren [" @@ lex
-  "foo constr:[[[xxx. (foo.+1 @@ [] ) \"]])\" yyy]]]."
-  ;
-  mk_bool_test (i2s __LINE__) "quotation nesting {" @@ lex
-  "bar:{{ foo {{ hello. }} }}."
-  ;
-
-]
-
-let _ = run_tests __FILE__ log_out_ch tests
diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
index d0b8d21b69..60267cd859 100644
--- a/test-suite/unit-tests/printing/proof_diffs_test.ml
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -76,11 +76,14 @@ let _ = add_test "tokenize_string/diff_mode in lexer" t
 
 open Pp
 
+let write_diffs_option s =
+  Goptions.set_string_option_value Proof_diffs.opt_name s
+
 (* example that was failing from #8922 *)
 let t () =
-  Proof_diffs.write_diffs_option "removed";
+  write_diffs_option "removed";
   ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1");
-  Proof_diffs.write_diffs_option "on"
+  write_diffs_option "on"
 let _ = add_test "shorten_diff_span failure from #8922" t
 
 (* note pp_to_string concatenates adjacent strings, could become one token,
@@ -181,7 +184,7 @@ let _ = if false then add_test "diff_pp/add_diff_tags token containing white spa
 
 let add_entries map idents rhs_pp =
   let make_entry() = { idents; rhs_pp; done_ = false } in
-  List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents;;
+  List.iter (fun ident -> map := (CString.Map.add ident (make_entry ()) !map); ()) idents;;
 
 let print_list hyps = List.iter (fun x -> cprintf "%s\n" (string_of_ppcmds (flatten x))) hyps
 let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (flatten x))) hyps
@@ -194,11 +197,11 @@ let db_print_list hyps = List.iter (fun x -> cprintf "%s\n" (db_string_of_pp (fl
 let t () =
   write_diffs_option "removed";   (* turn on "removed" option *)
   let o_line_idents = [ ["a"]; ["b"]] in
-  let o_hyp_map = ref StringMap.empty in
+  let o_hyp_map = ref CString.Map.empty in
   add_entries o_hyp_map ["a"] (str " : foo");
   add_entries o_hyp_map ["b"] (str " : bar car");
   let n_line_idents = [ ["b"]; ["a"]] in
-  let n_hyp_map = ref StringMap.empty in
+  let n_hyp_map = ref CString.Map.empty in
   add_entries n_hyp_map ["b"] (str " : car");
   add_entries n_hyp_map ["a"] (str " : foo bar");
   let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar")); str " car" ]));
@@ -224,11 +227,11 @@ let _ = add_test "diff_hyps simple diffs" t
 let t () =
   write_diffs_option "removed";   (* turn on "removed" option *)
   let o_line_idents = [ ["a"]; ["c"; "d"]] in
-  let o_hyp_map = ref StringMap.empty in
+  let o_hyp_map = ref CString.Map.empty in
   add_entries o_hyp_map ["a"] (str " : nat");
   add_entries o_hyp_map ["c"; "d"] (str " : int");
   let n_line_idents = [ ["a"; "b"]; ["d"]] in
-  let n_hyp_map = ref StringMap.empty in
+  let n_hyp_map = ref CString.Map.empty in
   add_entries n_hyp_map ["a"; "b"] (str " : nat");
   add_entries n_hyp_map ["d"] (str " : int");
   let expected = [flatten (wrap_in_bg "diff.added" (seq [str "a"; (tag "start.diff.added" (str ", ")); (tag "end.diff.added" (str "b")); str " : nat" ]));
@@ -264,12 +267,12 @@ DIFFS
 let t () =
   write_diffs_option "removed";   (* turn on "removed" option *)
   let o_line_idents = [ ["a"]; ["b"]; ["c"]] in
-  let o_hyp_map = ref StringMap.empty in
+  let o_hyp_map = ref CString.Map.empty in
   add_entries o_hyp_map ["a"] (str " : foo");
   add_entries o_hyp_map ["b"] (str " : bar");
   add_entries o_hyp_map ["c"] (str " : nat");
   let n_line_idents = [ ["b"; "a"; "c"] ] in
-  let n_hyp_map = ref StringMap.empty in
+  let n_hyp_map = ref CString.Map.empty in
   add_entries n_hyp_map ["b"; "a"; "c"] (str " : nat");
   let expected = [flatten (wrap_in_bg "diff.removed" (seq [str "b"; str " : "; (tag "diff.removed" (str "bar"))]));
                   flatten (wrap_in_bg "diff.added" (seq [str "b"; str " : "; (tag "diff.added" (str "nat"))]));
@@ -302,10 +305,10 @@ DIFFS
 let t () =
   write_diffs_option "removed";   (* turn on "removed" option *)
   let o_line_idents = [ ["b"; "a"; "c"] ] in
-  let o_hyp_map = ref StringMap.empty in
+  let o_hyp_map = ref CString.Map.empty in
   add_entries o_hyp_map ["b"; "a"; "c"] (str " : nat");
   let n_line_idents = [ ["a"]; ["b"]; ["c"]] in
-  let n_hyp_map = ref StringMap.empty in
+  let n_hyp_map = ref CString.Map.empty in
   add_entries n_hyp_map ["a"] (str " : foo");
   add_entries n_hyp_map ["b"] (str " : bar");
   add_entries n_hyp_map ["c"] (str " : nat");