aboutsummaryrefslogtreecommitdiff
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/Makefile7
-rw-r--r--test-suite/bugs/closed/bug_11935.v6
-rw-r--r--test-suite/output/Arguments_renaming.out6
-rw-r--r--test-suite/output/NotationsSigma.out40
-rw-r--r--test-suite/output/NotationsSigma.v22
-rw-r--r--test-suite/output/Search.out2
-rw-r--r--test-suite/output/UselessSyndef.out2
-rw-r--r--test-suite/output/UselessSyndef.v10
-rw-r--r--test-suite/output/bug_11934.out13
-rw-r--r--test-suite/output/bug_11934.v13
-rw-r--r--test-suite/success/PartialImport.v58
11 files changed, 171 insertions, 8 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index eade52b6eb..954a922c8c 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -354,8 +354,7 @@ $(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primit
} > "$@"
@if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi
$(HIDE)if ! grep -q -F "Error!" $@; then { \
- opts="$(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-I $(shell dirname $<) -norec $(shell basename $< .v))"; \
- $(coqchk) -silent $(call get_set_impredicativity,$<) $$opts 2>&1; R=$$?; \
+ $(coqchk) -silent $(call get_set_impredicativity,$<) $(if $(findstring modules/,$<),-R modules Mods -norec Mods.$(shell basename $< .v),-Q $(shell dirname $<) "" -norec $(shell basename $< .v)) 2>&1; R=$$?; \
if [ $$R != 0 ]; then \
echo $(log_failure); \
echo " $<...could not be checked (Error!)" ; \
@@ -381,7 +380,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
} > "$@"
@if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi
$(HIDE)if ! grep -q -F "Error!" $@; then { \
- $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \
+ $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \
if [ $$R != 0 ]; then \
echo $(log_failure); \
echo " $<...could not be checked (Error!)" ; \
@@ -405,7 +404,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
} > "$@"
@if ! grep -q -F "Error!" $@; then echo "CHECK $<"; fi
$(HIDE)if ! grep -q -F "Error!" $@; then { \
- $(coqchk) -silent -I $(shell dirname $<) -norec $(shell basename $< .v) 2>&1; R=$$?; \
+ $(coqchk) -silent -Q $(shell dirname $<) "" -norec $(shell basename $< .v) 2>&1; R=$$?; \
if [ $$R != 0 ]; then \
echo $(log_failure); \
echo " $<...could not be checked (Error!)" ; \
diff --git a/test-suite/bugs/closed/bug_11935.v b/test-suite/bugs/closed/bug_11935.v
new file mode 100644
index 0000000000..ad5ffc68b5
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11935.v
@@ -0,0 +1,6 @@
+Section S.
+ Variable A : Prop.
+
+ Fail Check A@{Type}.
+ Check A@{}.
+End S.
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index abc7f0f88e..e0aa758812 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -2,9 +2,9 @@ The command has indeed failed with message:
Flag "rename" expected to rename A into B.
File "stdin", line 3, characters 0-25:
Warning: This command is just asserting the names of arguments of identity.
-If this is what you want add ': assert' to silence the warning. If you want
-to clear implicit arguments add ': clear implicits'. If you want to clear
-notation scopes add ': clear scopes' [arguments-assert,vernacular]
+If this is what you want, add ': assert' to silence the warning. If you want
+to clear implicit arguments, add ': clear implicits'. If you want to clear
+notation scopes, add ': clear scopes' [arguments-assert,vernacular]
@eq_refl
: forall (B : Type) (y : B), y = y
eq_refl
diff --git a/test-suite/output/NotationsSigma.out b/test-suite/output/NotationsSigma.out
new file mode 100644
index 0000000000..0e4df87148
--- /dev/null
+++ b/test-suite/output/NotationsSigma.out
@@ -0,0 +1,40 @@
+{0 = 0} + {0 < 1}
+ : Set
+(0 = 0) + {0 < 1}
+ : Set
+{x : nat | x = 1}
+ : Set
+{x : nat | x = 1 & 0 < x}
+ : Set
+{x : nat | x = 1}
+ : Set
+{x : nat | x = 1 & 0 < x}
+ : Set
+{x : nat & x = 1}
+ : Set
+{x : nat & x = 1 & 0 < x}
+ : Set
+{x : nat & x = 1}
+ : Set
+{x : nat & x = 1 & 0 < x}
+ : Set
+{'(x, _) : nat * ?T | x = 1}
+ : Type
+where
+?T : [pat : nat * ?T |- Type] (pat cannot be used)
+{'(x, y) : nat * nat | x = 1 & y = 0}
+ : Set
+{'(x, _) : nat * nat | x = 1}
+ : Set
+{'(x, y) : nat * nat | x = 1 & y = 0}
+ : Set
+{'(x, _) : nat * ?T & x = 1}
+ : Type
+where
+?T : [pat : nat * ?T |- Type] (pat cannot be used)
+{'(x, y) : nat * nat & x = 1 & y = 0}
+ : Type
+{'(x, _) : nat * nat & x = 1}
+ : Type
+{'(x, y) : nat * nat & x = 1 & y = 0}
+ : Type
diff --git a/test-suite/output/NotationsSigma.v b/test-suite/output/NotationsSigma.v
new file mode 100644
index 0000000000..6780d63a04
--- /dev/null
+++ b/test-suite/output/NotationsSigma.v
@@ -0,0 +1,22 @@
+(* Check notations for sigma types *)
+
+Check { 0 = 0 } + { 0 < 1 }.
+Check (0 = 0) + { 0 < 1 }.
+
+Check { x | x = 1 }.
+Check { x | x = 1 & 0 < x }.
+Check { x : nat | x = 1 }.
+Check { x : nat | x = 1 & 0 < x }.
+Check { x & x = 1 }.
+Check { x & x = 1 & 0 < x }.
+Check { x : nat & x = 1 }.
+Check { x : nat & x = 1 & 0 < x }.
+
+Check {'(x,y) | x = 1 }.
+Check {'(x,y) | x = 1 & y = 0 }.
+Check {'(x,y) : nat * nat | x = 1 }.
+Check {'(x,y) : nat * nat | x = 1 & y = 0 }.
+Check {'(x,y) & x = 1 }.
+Check {'(x,y) & x = 1 & y = 0 }.
+Check {'(x,y) : nat * nat & x = 1 }.
+Check {'(x,y) : nat * nat & x = 1 & y = 0 }.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 9d8e830d64..593d0c7f67 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -136,7 +136,7 @@ h': newdef n <> n
(use "About" for full details on implicit arguments)
(use "About" for full details on implicit arguments)
The command has indeed failed with message:
-No such goal.
+[Focus] No such goal.
The command has indeed failed with message:
Query commands only support the single numbered goal selector.
The command has indeed failed with message:
diff --git a/test-suite/output/UselessSyndef.out b/test-suite/output/UselessSyndef.out
new file mode 100644
index 0000000000..ce484889b3
--- /dev/null
+++ b/test-suite/output/UselessSyndef.out
@@ -0,0 +1,2 @@
+a
+ : nat
diff --git a/test-suite/output/UselessSyndef.v b/test-suite/output/UselessSyndef.v
new file mode 100644
index 0000000000..96ad6e9f5c
--- /dev/null
+++ b/test-suite/output/UselessSyndef.v
@@ -0,0 +1,10 @@
+Module M.
+ Definition a := 0.
+End M.
+Module N.
+ Notation a := M.a (only parsing).
+End N.
+
+Import M. Import N.
+
+Check a.
diff --git a/test-suite/output/bug_11934.out b/test-suite/output/bug_11934.out
new file mode 100644
index 0000000000..072136c82e
--- /dev/null
+++ b/test-suite/output/bug_11934.out
@@ -0,0 +1,13 @@
+thing = forall x y : foo, bla x y
+ : Prop
+thing =
+forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y
+ : Prop
+(* {thing.u1 thing.u0} |= bla.u0 = thing.u0
+ bla.u1 = thing.u1 *)
+thing =
+forall (x : @foo@{thing.u0} True) (y : @foo@{thing.u1} True),
+@bla True True x y
+ : Prop
+(* {thing.u1 thing.u0} |= bla.u0 = thing.u0
+ bla.u1 = thing.u1 *)
diff --git a/test-suite/output/bug_11934.v b/test-suite/output/bug_11934.v
new file mode 100644
index 0000000000..fe9772dc62
--- /dev/null
+++ b/test-suite/output/bug_11934.v
@@ -0,0 +1,13 @@
+Polymorphic Axiom foo@{u} : Prop -> Prop.
+Arguments foo {_}.
+
+Axiom bla : forall {A B}, @foo A -> @foo B -> Prop.
+Definition thing := forall (x:@foo@{Type} True) (y:@foo@{Type} True), bla x y.
+
+Print thing. (* forall x y : foo, bla x y *)
+
+Set Printing Universes.
+Print thing. (* forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y *)
+
+Set Printing Implicit.
+Print thing. (* BAD: forall x y : @foo@{thing.u0} True, @bla True True x y *)
diff --git a/test-suite/success/PartialImport.v b/test-suite/success/PartialImport.v
new file mode 100644
index 0000000000..720083aec5
--- /dev/null
+++ b/test-suite/success/PartialImport.v
@@ -0,0 +1,58 @@
+Module M.
+
+ Definition a := 0.
+ Definition b := 1.
+
+ Module N.
+
+ Notation c := (a + b).
+
+ End N.
+
+ Inductive even : nat -> Prop :=
+ | even_0 : even 0
+ | even_S n : odd n -> even (S n)
+ with odd : nat -> Set :=
+ odd_S n : even n -> odd (S n).
+
+End M.
+
+Module Simple.
+
+ Import M(a).
+
+ Check a.
+ Fail Check b.
+ Fail Check N.c.
+
+ (* todo output test: this prints a+M.b since the notation isn't imported *)
+ Check M.N.c.
+
+ Fail Import M(c).
+ Fail Import M(M.b).
+
+ Import M(N.c).
+ Check N.c.
+ (* interestingly prints N.c (also does with unfiltered Import M) *)
+
+ Import M(even(..)).
+ Check even. Check even_0. Check even_S.
+ Check even_sind. Check even_ind.
+ Fail Check even_rect. (* doesn't exist *)
+ Fail Check odd. Check M.odd.
+ Fail Check odd_S. Fail Check odd_sind.
+
+End Simple.
+
+Module WithExport.
+
+ Module X.
+ Export M(a, N.c).
+ End X.
+
+ Import X.
+ Check a.
+ Check N.c. (* also prints N.c *)
+ Fail Check b.
+
+End WithExport.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 12:52:22 +0000