aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/bugs/closed/bug_10669.v12
-rw-r--r--test-suite/bugs/closed/bug_10888.v11
-rw-r--r--test-suite/output-coqtop/DependentEvars.out91
-rw-r--r--test-suite/output-coqtop/DependentEvars.v24
-rw-r--r--test-suite/output-coqtop/DependentEvars2.out120
-rw-r--r--test-suite/output-coqtop/DependentEvars2.v27
-rw-r--r--test-suite/output/UnivBinders.out38
-rw-r--r--test-suite/success/CompatCurrentFlag.v4
-rw-r--r--test-suite/success/CompatOldFlag.v4
-rw-r--r--test-suite/success/CompatOldOldFlag.v6
-rw-r--r--test-suite/success/CompatPreviousFlag.v4
-rwxr-xr-xtest-suite/tools/update-compat/run.sh2
12 files changed, 317 insertions, 26 deletions
diff --git a/test-suite/bugs/closed/bug_10669.v b/test-suite/bugs/closed/bug_10669.v
new file mode 100644
index 0000000000..433e300acb
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10669.v
@@ -0,0 +1,12 @@
+
+Context (A0:Type) (B0:A0).
+Definition foo0 := B0.
+
+Set Universe Polymorphism.
+Context (A1:Type) (B1:A1).
+Definition foo1 := B1.
+
+Section S.
+ Context (A2:Type) (B2:A2).
+ Definition foo2 := B2.
+End S.
diff --git a/test-suite/bugs/closed/bug_10888.v b/test-suite/bugs/closed/bug_10888.v
new file mode 100644
index 0000000000..3c2e8011d7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10888.v
@@ -0,0 +1,11 @@
+
+Module Type T.
+Context {A:Type}.
+End T.
+
+Module M(X:T).
+ Import X.
+ Check X.A.
+ Check A.
+ Definition B := A.
+End M.
diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out
new file mode 100644
index 0000000000..9ca3fa3357
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.out
@@ -0,0 +1,91 @@
+
+Coq <
+Coq < Coq < 1 subgoal
+
+ ============================
+ forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans <
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans <
+Coq < Coq < 1 subgoal
+
+ ============================
+ forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon <
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon <
+Coq < Coq <
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+
+ P1, P2, P3, P4 : Prop
+ p12 : P1 -> P2
+ p123 : (P1 -> P2) -> P3
+ p34 : P3 -> P4
+ ============================
+ P4
+
+(dependent evars: ; in current goal:)
+
+p14 <
+p14 < 4 focused subgoals
+(shelved: 2)
+
+ P1, P2, P3, P4 : Prop
+ p12 : P1 -> P2
+ p123 : (P1 -> P2) -> P3
+ p34 : P3 -> P4
+ ============================
+ ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+
+ P1, P2, P3, P4 : Prop
+ p12 : P1 -> P2
+ p123 : (P1 -> P2) -> P3
+ p34 : P3 -> P4
+ ============================
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 <
+Coq <
+Coq <
diff --git a/test-suite/output-coqtop/DependentEvars.v b/test-suite/output-coqtop/DependentEvars.v
new file mode 100644
index 0000000000..5a59054073
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.v
@@ -0,0 +1,24 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+ forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+ auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+ tauto.
+Qed.
+
+Section eex.
+ Variables P1 P2 P3 P4 : Prop.
+ Hypothesis p12 : P1 -> P2.
+ Hypothesis p123 : (P1 -> P2) -> P3.
+ Hypothesis p34 : P3 -> P4.
+
+ Lemma p14 : P4.
+ Proof.
+ eapply strange_imp_trans.
+ apply modpon.
+ Abort.
+End eex.
diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out
new file mode 100644
index 0000000000..29ebba7c86
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.out
@@ -0,0 +1,120 @@
+
+Coq <
+Coq < Coq < 1 subgoal
+
+ ============================
+ forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans <
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans <
+Coq < Coq < 1 subgoal
+
+ ============================
+ forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon <
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon <
+Coq < Coq <
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+
+ P1, P2, P3, P4 : Prop
+ p12 : P1 -> P2
+ p123 : (P1 -> P2) -> P3
+ p34 : P3 -> P4
+ ============================
+ P4
+
+(dependent evars: ; in current goal:)
+
+p14 <
+p14 < Second proof:
+
+p14 < 4 focused subgoals
+(shelved: 2)
+
+ P1, P2, P3, P4 : Prop
+ p12 : P1 -> P2
+ p123 : (P1 -> P2) -> P3
+ p34 : P3 -> P4
+ ============================
+ ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 1 focused subgoal
+(shelved: 2)
+
+ P1, P2, P3, P4 : Prop
+ p12 : P1 -> P2
+ p123 : (P1 -> P2) -> P3
+ p34 : P3 -> P4
+ ============================
+ ?Q -> P4
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < This subproof is complete, but there are some unfocused goals.
+Try unfocusing with "}".
+
+3 subgoals
+(shelved: 2)
+
+subgoal 1 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+
+ P1, P2, P3, P4 : Prop
+ p12 : P1 -> P2
+ p123 : (P1 -> P2) -> P3
+ p34 : P3 -> P4
+ ============================
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 <
+Coq <
+Coq <
diff --git a/test-suite/output-coqtop/DependentEvars2.v b/test-suite/output-coqtop/DependentEvars2.v
new file mode 100644
index 0000000000..d0f3a4012e
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.v
@@ -0,0 +1,27 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+ forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+ auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+ tauto.
+Qed.
+
+Section eex.
+ Variables P1 P2 P3 P4 : Prop.
+ Hypothesis p12 : P1 -> P2.
+ Hypothesis p123 : (P1 -> P2) -> P3.
+ Hypothesis p34 : P3 -> P4.
+
+ Lemma p14 : P4.
+ Proof.
+ idtac "Second proof:".
+ eapply strange_imp_trans.
+ {
+ apply modpon.
+ }
+ Abort.
+End eex.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index a89fd64999..d48d8b900f 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -38,10 +38,10 @@ Argument scopes are [type_scope _]
bar@{u} = nat
: Wrap@{u} Set
(* u |= Set < u *)
-foo@{u UnivBinders.17 v} =
-Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
- : Type@{max(u+1,UnivBinders.17+1,v+1)}
-(* u UnivBinders.17 v |= *)
+foo@{u UnivBinders.18 v} =
+Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
+ : Type@{max(u+1,UnivBinders.18+1,v+1)}
+(* u UnivBinders.18 v |= *)
Type@{i} -> Type@{j}
: Type@{max(i+1,j+1)}
(* {j i} |= *)
@@ -68,19 +68,19 @@ mono
The command has indeed failed with message:
Universe u already exists.
bobmorane =
-let tt := Type@{UnivBinders.33} in
-let ff := Type@{UnivBinders.35} in tt -> ff
- : Type@{max(UnivBinders.32,UnivBinders.34)}
+let tt := Type@{UnivBinders.34} in
+let ff := Type@{UnivBinders.36} in tt -> ff
+ : Type@{max(UnivBinders.33,UnivBinders.35)}
The command has indeed failed with message:
Universe u already bound.
foo@{E M N} =
Type@{M} -> Type@{N} -> Type@{E}
: Type@{max(E+1,M+1,N+1)}
(* E M N |= *)
-foo@{u UnivBinders.17 v} =
-Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
- : Type@{max(u+1,UnivBinders.17+1,v+1)}
-(* u UnivBinders.17 v |= *)
+foo@{u UnivBinders.18 v} =
+Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
+ : Type@{max(u+1,UnivBinders.18+1,v+1)}
+(* u UnivBinders.18 v |= *)
Inductive Empty@{E} : Type@{E} :=
(* E |= *)
Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
@@ -143,26 +143,26 @@ Applied.infunct@{u v} =
inmod@{u} -> Type@{v}
: Type@{max(u+1,v+1)}
(* u v |= *)
-axfoo@{i UnivBinders.57 UnivBinders.58} :
-Type@{UnivBinders.57} -> Type@{i}
-(* i UnivBinders.57 UnivBinders.58 |= *)
+axfoo@{i UnivBinders.59 UnivBinders.60} :
+Type@{UnivBinders.59} -> Type@{i}
+(* i UnivBinders.59 UnivBinders.60 |= *)
axfoo is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.57 UnivBinders.58} :
-Type@{UnivBinders.58} -> Type@{i}
-(* i UnivBinders.57 UnivBinders.58 |= *)
+axbar@{i UnivBinders.59 UnivBinders.60} :
+Type@{UnivBinders.60} -> Type@{i}
+(* i UnivBinders.59 UnivBinders.60 |= *)
axbar is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
axfoo' is not universe polymorphic
Argument scope is [type_scope]
Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
axbar' is not universe polymorphic
Argument scope is [type_scope]
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index 81469d79c3..fd6101bf89 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
(** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq811.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index afeb57f9f2..f774cef44f 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
(** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq811.
Import Coq.Compat.Coq810.
Import Coq.Compat.Coq89.
-Import Coq.Compat.Coq88.
diff --git a/test-suite/success/CompatOldOldFlag.v b/test-suite/success/CompatOldOldFlag.v
new file mode 100644
index 0000000000..20eef955b4
--- /dev/null
+++ b/test-suite/success/CompatOldOldFlag.v
@@ -0,0 +1,6 @@
+(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(** Check that the current-minus-three compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq811.
+Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq89.
+Import Coq.Compat.Coq88.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index c8f75915c8..1c5ccc1a92 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
(** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq811.
Import Coq.Compat.Coq810.
-Import Coq.Compat.Coq89.
diff --git a/test-suite/tools/update-compat/run.sh b/test-suite/tools/update-compat/run.sh
index 7ff5571ffb..61273c4f37 100755
--- a/test-suite/tools/update-compat/run.sh
+++ b/test-suite/tools/update-compat/run.sh
@@ -6,4 +6,4 @@ SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null && pwd )"
# we assume that the script lives in test-suite/tools/update-compat/,
# and that update-compat.py lives in dev/tools/
cd "${SCRIPT_DIR}/../../.."
-dev/tools/update-compat.py --assert-unchanged --release || exit $?
+dev/tools/update-compat.py --assert-unchanged --master || exit $?
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 13:24:45 +0000