aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_13755.v5
-rwxr-xr-xtest-suite/misc/non-marshalable-state.sh30
-rw-r--r--test-suite/misc/non-marshalable-state/_CoqProject9
-rw-r--r--test-suite/misc/non-marshalable-state/src/evil.mlg15
-rw-r--r--test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack1
-rw-r--r--test-suite/misc/non-marshalable-state/src/good.mlg16
-rw-r--r--test-suite/misc/non-marshalable-state/src/good_plugin.mlpack1
-rw-r--r--test-suite/misc/non-marshalable-state/theories/evil.v5
-rw-r--r--test-suite/misc/non-marshalable-state/theories/good.v5
-rw-r--r--test-suite/output/SearchHead.v19
-rw-r--r--test-suite/output/Search_headconcl.out (renamed from test-suite/output/SearchHead.out)20
-rw-r--r--test-suite/output/Search_headconcl.v18
-rw-r--r--test-suite/success/induct.v44
13 files changed, 105 insertions, 83 deletions
diff --git a/test-suite/bugs/closed/bug_13755.v b/test-suite/bugs/closed/bug_13755.v
new file mode 100644
index 0000000000..cc25157b9b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13755.v
@@ -0,0 +1,5 @@
+Module M1.
+Lemma t1 : True.
+Fail End M1.
+Proof. exact I. Qed.
+End M1.
diff --git a/test-suite/misc/non-marshalable-state.sh b/test-suite/misc/non-marshalable-state.sh
new file mode 100755
index 0000000000..eef7786ebc
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state.sh
@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+
+set -e
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+cd misc/non-marshalable-state/
+
+coq_makefile -f _CoqProject -o Makefile
+
+make clean
+
+make src/evil_plugin.cmxs
+make src/good_plugin.cmxs
+
+RC=1
+# must fail
+coqc -async-proofs on -I src -Q theories Marshal theories/evil.v 2> log1 1>&2 || RC=0
+# for this reason
+grep -q 'Marshalling error' log1 || RC=1
+
+# must work
+coqc -async-proofs off -I src -Q theories Marshal theories/evil.v
+
+# must work
+coqc -async-proofs on -I src -Q theories Marshal theories/good.v
+
+
+exit $RC
diff --git a/test-suite/misc/non-marshalable-state/_CoqProject b/test-suite/misc/non-marshalable-state/_CoqProject
new file mode 100644
index 0000000000..09e68d866c
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/_CoqProject
@@ -0,0 +1,9 @@
+-Q theories Marshal
+-I src
+
+src/evil.mlg
+src/good.mlg
+src/evil_plugin.mlpack
+src/good_plugin.mlpack
+theories/evil.v
+theories/good.v
diff --git a/test-suite/misc/non-marshalable-state/src/evil.mlg b/test-suite/misc/non-marshalable-state/src/evil.mlg
new file mode 100644
index 0000000000..59b2b5a8ac
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/evil.mlg
@@ -0,0 +1,15 @@
+DECLARE PLUGIN "evil_plugin"
+
+{
+
+let state = Summary.ref
+ ~name:"elpi-compiler-cache"
+ None
+
+}
+
+VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF
+| [ "magic" ] -> {
+ state := Some (fun () -> ())
+}
+END
diff --git a/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack
new file mode 100644
index 0000000000..6382aa69e1
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/evil_plugin.mlpack
@@ -0,0 +1 @@
+Evil
diff --git a/test-suite/misc/non-marshalable-state/src/good.mlg b/test-suite/misc/non-marshalable-state/src/good.mlg
new file mode 100644
index 0000000000..c6b9cbefd5
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/good.mlg
@@ -0,0 +1,16 @@
+DECLARE PLUGIN "good_plugin"
+
+{
+
+let state = Summary.Local.ref
+ ~name:"elpi-compiler-cache"
+ None
+
+}
+
+VERNAC COMMAND EXTEND magic CLASSIFIED AS SIDEFF
+| [ "magic" ] -> {
+ let open Summary.Local in
+ state := Some (fun () -> ())
+}
+END
diff --git a/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack
new file mode 100644
index 0000000000..cd9dd73b78
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/src/good_plugin.mlpack
@@ -0,0 +1 @@
+Good
diff --git a/test-suite/misc/non-marshalable-state/theories/evil.v b/test-suite/misc/non-marshalable-state/theories/evil.v
new file mode 100644
index 0000000000..661482a975
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/theories/evil.v
@@ -0,0 +1,5 @@
+Declare ML Module "evil_plugin".
+
+magic.
+
+Lemma x : True. Proof. trivial. Qed.
diff --git a/test-suite/misc/non-marshalable-state/theories/good.v b/test-suite/misc/non-marshalable-state/theories/good.v
new file mode 100644
index 0000000000..eab9a043e1
--- /dev/null
+++ b/test-suite/misc/non-marshalable-state/theories/good.v
@@ -0,0 +1,5 @@
+Declare ML Module "good_plugin".
+
+magic.
+
+Lemma x : True. Proof. trivial. Qed.
diff --git a/test-suite/output/SearchHead.v b/test-suite/output/SearchHead.v
deleted file mode 100644
index 2ee8a0d184..0000000000
--- a/test-suite/output/SearchHead.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* Some tests of the Search command *)
-
-SearchHead le. (* app nodes *)
-SearchHead bool. (* no apps *)
-SearchHead (@eq nat). (* complex pattern *)
-
-Definition newdef := fun x:nat => x = x.
-
-Goal forall n:nat, newdef n -> False.
- intros n h.
- SearchHead newdef. (* search hypothesis *)
-Abort.
-
-
-Goal forall n (P:nat -> Prop), P n -> False.
- intros n P h.
- SearchHead P. (* search hypothesis also for patterns *)
-Abort.
-
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/Search_headconcl.out
index 2f0d854ac6..24e2ee76af 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/Search_headconcl.out
@@ -1,17 +1,9 @@
-File "stdin", line 3, characters 0-14:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
le_n: forall n : nat, n <= n
le_0_n: forall n : nat, 0 <= n
le_S: forall n m : nat, n <= m -> n <= S m
le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
le_n_S: forall n m : nat, n <= m -> S n <= S m
le_S_n: forall n m : nat, S n <= S m -> n <= m
-File "stdin", line 4, characters 0-16:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
false: bool
true: bool
negb: bool -> bool
@@ -35,10 +27,6 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool
Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool
Decimal.int_beq: Decimal.int -> Decimal.int -> bool
Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool
-File "stdin", line 5, characters 0-21:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
mult_n_O: forall n : nat, 0 = n * 0
plus_O_n: forall n : nat, 0 + n = n
plus_n_O: forall n : nat, n = n + 0
@@ -57,13 +45,5 @@ f_equal2_plus:
forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
f_equal2_mult:
forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-File "stdin", line 11, characters 2-20:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
h: newdef n
-File "stdin", line 17, characters 2-15:
-Warning:
-SearchHead is deprecated. Use the headconcl: clause of Search instead.
-[deprecated-searchhead,deprecated]
h: P n
diff --git a/test-suite/output/Search_headconcl.v b/test-suite/output/Search_headconcl.v
new file mode 100644
index 0000000000..8b168dcd25
--- /dev/null
+++ b/test-suite/output/Search_headconcl.v
@@ -0,0 +1,18 @@
+(* Some tests of the Search command *)
+
+Search headconcl: le. (* app nodes *)
+Search headconcl: bool. (* no apps *)
+Search headconcl: (@eq nat). (* complex pattern *)
+
+Definition newdef := fun x:nat => x = x.
+
+Goal forall n:nat, newdef n -> False.
+ intros n h.
+ Search headconcl: newdef. (* search hypothesis *)
+Abort.
+
+
+Goal forall n (P:nat -> Prop), P n -> False.
+ intros n P h.
+ Search headconcl: P. (* search hypothesis also for patterns *)
+Abort.
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 4983ee3c0d..615350c58c 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -154,50 +154,6 @@ induction H.
change (0 = z -> True) in IHrepr''.
Abort.
-(* Test double induction *)
-
-(* This was failing in 8.5 and before because of a bug in the order of
- hypotheses *)
-
-Set Warnings "-deprecated".
-
-Inductive I2 : Type :=
- C2 : forall x:nat, x=x -> I2.
-Goal forall a b:I2, a = b.
-double induction a b.
-Abort.
-
-(* This was leaving useless hypotheses in 8.5 and before because of
- the same bug. This is a change of compatibility. *)
-
-Inductive I3 : Prop :=
- C3 : forall x:nat, x=x -> I3.
-Goal forall a b:I3, a = b.
-double induction a b.
-Fail clear H. (* H should have been erased *)
-Abort.
-
-(* This one had quantification in reverse order in 8.5 and before *)
-(* This is a change of compatibility. *)
-
-Goal forall m n, le m n -> le n m -> n=m.
-intros m n. double induction 1 2.
-3:destruct 1. (* Should be "S m0 <= m0" *)
-Abort.
-
-(* Idem *)
-
-Goal forall m n p q, le m n -> le p q -> n+p=m+q.
-intros *. double induction 1 2.
-3:clear H2. (* H2 should have been erased *)
-Abort.
-
-(* This is unchanged *)
-
-Goal forall m n:nat, n=m.
-double induction m n.
-Abort.
-
(* Mentioned as part of bug #12944 *)
Inductive test : Set := cons : forall (IHv : nat) (v : test), test.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 04:12:48 +0000