Add simple clear test for multiple files without require

5 files changed, 54 insertions, 11 deletions

diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index fa48159a..351b66ce 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -32,27 +32,32 @@
   (pg-autotest eval (proof-electric-terminator-toggle 1))
   (pg-autotest eval (insert "Module test")) ; no \n
   (proof-electric-terminator)
+  (proof-shell-wait)
   (pg-autotest eval (insert " Goal forall (A B:Prop),(A /\\ B) -> (B /\\ A)"))
   (proof-electric-terminator)
+  (proof-shell-wait)
   (pg-autotest eval (insert "\ntauto."))
-  ; FIXME: bug here
-  ; (backward-char)
-  ; (proof-electric-terminator) ; shouldn't insert another or delete present
-  (pg-autotest eval (proof-goto-point))
+  (backward-char)
+  (proof-electric-terminator) ; shouldn't insert another or delete present
   (proof-shell-wait)
-  ;; FIXME: next test fails, why?
-  ;; (pg-autotest assert-full)
+;; FIXME: next test fails, why?
+  (pg-autotest assert-full)
   ;; TODO: test switching active scripting buffer after
   ;; an error (see cvs log for proof-script.el 10.68)
-  (pg-autotest eval (insert " End test"))
-  (proof-electric-terminator)
+;; FIXME: bug, this causes "region is read only"
+;;  (pg-autotest eval (insert " End test"))
+;;  (proof-electric-terminator)
   (set-buffer-modified-p nil)
   (kill-buffer ".autotest.v")
   (proof-shell-wait)
 
-  ;; FIXME: this is broken too: retracting a previously
-  ;; processed file doesn't seem to work
-  ;; (pg-autotest script-wholefile "coq/example.v")
+  
+  (pg-autotest script-wholefile "etc/coq/multiple-plain/a.v")
+  (pg-autotest script-wholefile "etc/coq/multiple-plain/b.v")
+  (pg-autotest script-wholefile "etc/coq/multiple-plain/c.v")
+  ;; FIXME: this is broken: retracting a previously
+  ;; processed file doesn't work
+  (pg-autotest script-wholefile "etc/coq/multiple-plain/a.v")
 
   (pg-autotest quit-prover)
 
diff --git a/etc/coq/multiple-plain/README b/etc/coq/multiple-plain/README
new file mode 100644
index 00000000..6c37325b
--- /dev/null
+++ b/etc/coq/multiple-plain/README
@@ -0,0 +1,8 @@
+Plain tests for multiple file handling, without using require.
+
+Test:
+
+ process a.v
+ process b.v
+ undo a.v, redo a.v
+
diff --git a/etc/coq/multiple-plain/a.v b/etc/coq/multiple-plain/a.v
new file mode 100644
index 00000000..d628156e
--- /dev/null
+++ b/etc/coq/multiple-plain/a.v
@@ -0,0 +1,10 @@
+(* Simple tests for multiple file handling *)
+
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
+  intros A B H.
+  elim H.
+  intros.
+  split.
+  assumption.
+  assumption.
+Save and_comms_a.
diff --git a/etc/coq/multiple-plain/b.v b/etc/coq/multiple-plain/b.v
new file mode 100644
index 00000000..aadfeedb
--- /dev/null
+++ b/etc/coq/multiple-plain/b.v
@@ -0,0 +1,10 @@
+(* Simple tests for multiple file handling *)
+
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
+  intros A B H.
+  elim H.
+  intros.
+  split.
+  assumption.
+  assumption.
+Save and_comms_b.
diff --git a/etc/coq/multiple-plain/c.v b/etc/coq/multiple-plain/c.v
new file mode 100644
index 00000000..93bf9895
--- /dev/null
+++ b/etc/coq/multiple-plain/c.v
@@ -0,0 +1,10 @@
+(* Simple tests for multiple file handling *)
+
+Goal forall (A B:Prop),(A /\ B) -> (B /\ A).
+  intros A B H.
+  elim H.
+  intros.
+  split.
+  assumption.
+  assumption.
+Save and_comms_c.