Correct messages for assumption tests with CWStopOnFailure 0

Author: monadius

cw_example/Preloaded.v

@@ -1 +1,2 @@
-Axiom test_axiom : False.
+Axiom test_axiom : False.
+Axiom another_axiom : False.

cw_example/Solution.v

@@ -1,4 +1,7 @@
 Require Import Preloaded.
 
 Lemma solution : 1 + 1 = 3.
-Proof. firstorder using test_axiom. Qed.
+Proof. firstorder using test_axiom. Qed.
+
+Lemma solution2 : 1 + 1 = 3 /\ 2 + 2 = 4.
+Proof. split; [firstorder using test_axiom | firstorder using another_axiom]. Qed.

cw_example/SolutionTest.v

@@ -12,7 +12,11 @@ CWGroup "Tests for Solution.solution".
   (* CWEndTest is optional before CWTest or CWEndGroup *)
   CWEndTest.
   CWTest "Assumptions test".
-    CWAssert "Testing solution" Solution.solution Assumes. (*test_axiom.*)
+    CWAssert "Testing solution" Solution.solution Assumes test_axiom.
+    CWAssert "Testing solution (failure)" Solution.solution Assumes. (*test_axiom.*)
+    CWAssert "Testing solution2" Solution.solution2 Assumes test_axiom another_axiom.
+    CWAssert "Testing solution2 (failure 1)" Solution.solution2 Assumes test_axiom.
+    CWAssert "Testing solution2 (failure 2)" Solution.solution2 Assumes.
   CWTest "Type test 2".
     Definition expected := 1 + 1 = 3.
     CWAssert Solution.solution : expected.

src/coq_cw.ml

@@ -109,18 +109,20 @@ let test_axioms ?(msg = "Axiom Test") c_ref ax_refs =
   let ax_objs = List.map (fun c -> Printer.Axiom (Printer.Constant c, [])) ax_csts in
   let ax_set = Printer.ContextObjectSet.of_list ax_objs in
   let assums = assumptions c_ref in
-  let iter t ty =
+  let iter t ty axioms =
     match t with
     | Printer.Axiom (ax, _) ->
-      if Printer.ContextObjectSet.mem t ax_set then ()
+      if Printer.ContextObjectSet.mem t ax_set then axioms
       else begin
         let p_axiom = pr_axiom env sigma ax ty in
-        failed (Printf.sprintf "%s\nProhibited Axiom: %s" msg (string_of_ppcmds p_axiom))
+        string_of_ppcmds p_axiom :: axioms
       end
-    | _ -> ()
+    | _ -> axioms
   in
-  let () = Printer.ContextObjectMap.iter iter assums in
-  passed msg
+  let axioms = Printer.ContextObjectMap.fold_left iter assums [] in
+  match axioms with
+  | [] -> passed msg
+  | _ -> failed (Printf.sprintf "%s\nProhibited Axioms: %s" msg (String.concat "\n" axioms))
 
 (** Tests that the file size is less than a given number *)
 let test_file_size ?(fname = solution_file) size =