aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/Cases.v1
-rw-r--r--test-suite/output/Errors.out8
-rw-r--r--test-suite/output/Errors.v6
-rw-r--r--test-suite/output/Notations3.out18
-rw-r--r--test-suite/output/Notations3.v21
-rw-r--r--test-suite/output/Projections.out2
-rw-r--r--test-suite/output/Projections.v11
-rw-r--r--test-suite/output/UnclosedBlocks.out1
-rw-r--r--test-suite/output/bug5778.out4
-rw-r--r--test-suite/output/bug6404.out4
-rw-r--r--test-suite/output/bug6404.v7
-rw-r--r--test-suite/output/ltac.v3
-rw-r--r--test-suite/output/ssr_clear.out3
-rw-r--r--test-suite/output/ssr_clear.v6
-rw-r--r--test-suite/output/ssr_explain_match.out55
-rw-r--r--test-suite/output/ssr_explain_match.v23
16 files changed, 170 insertions, 3 deletions
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index caf3b28701..4740c009a4 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -163,6 +163,7 @@ match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end)
match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
Show.
+Abort.
Lemma lem5 (p:nat) : eq_refl p = eq_refl p.
let y := fresh "n" in (* Checking that y is hidden *)
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 38d055b28e..24180c4553 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -8,3 +8,11 @@ Unable to unify "nat" with "True".
The command has indeed failed with message:
Ltac call to "instantiate ( (ident) := (lglob) )" failed.
Instance is not well-typed in the environment of ?x.
+The command has indeed failed with message:
+Cannot infer the domain of the type of f.
+The command has indeed failed with message:
+Cannot infer the domain of the implicit parameter A of id whose type is
+"Type".
+The command has indeed failed with message:
+Cannot infer the codomain of the type of f in environment:
+x : nat
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 424d24801c..c9b5091347 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -25,3 +25,9 @@ eexists ?[x].
destruct H1 as [x1 H1].
Fail instantiate (x:=projT1 x1).
Abort.
+
+(* Test some messages for non solvable evars *)
+
+Fail Goal forall a f, f a = 0.
+Fail Goal forall f x, id f x = 0.
+Fail Goal forall f P, P (f 0).
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 1987b6a6e9..996af59270 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -223,3 +223,21 @@ fun S : nat => [[S | S.S]]
: Set
exists2 '{{y, z}} : nat * nat, y > z & z > y
: Prop
+foo =
+fun l : list nat => match l with
+ | _ :: (_ :: _) as l1 => l1
+ | _ => l
+ end
+ : list nat -> list nat
+
+Argument scope is [list_scope]
+Notation
+"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
+(default interpretation)
+"'exists' ! x .. y , p" := ex
+ (unique
+ (fun x => .. (ex (unique (fun y => p))) ..))
+: type_scope (default interpretation)
+Notation
+"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope
+(default interpretation)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index c165f9553e..3cf0c913f7 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -278,10 +278,12 @@ Set Printing Notations.
(* Check insensitivity of "match" clauses to order *)
+Module IfPat.
Notation "'if' t 'is' n .+ 1 'then' p 'else' q" :=
(match t with S n => p | 0 => q end)
(at level 200).
Check fun x => if x is n.+1 then n else 1.
+End IfPat.
(* Examples with binding patterns *)
@@ -338,11 +340,13 @@ Check ∀ '(((x,y),true)|((x,y),false)), x>y.
(* Check Georges' printability of a "if is then else" notation *)
+Module IfPat2.
Notation "'if' c 'is' p 'then' u 'else' v" :=
(match c with p => u | _ => v end)
(at level 200, p pattern at level 100).
Check fun p => if p is S n then n else 0.
Check fun p => if p is Lt then 1 else 0.
+End IfPat2.
(* Check that mixed binders and terms defaults to ident and not pattern *)
Module F.
@@ -364,3 +368,20 @@ Check {'(x,y)|x+y=0}.
(* Check exists2 with a pattern *)
Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
+
+Module Issue7110.
+Open Scope list_scope.
+Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..)
+ (at level 0).
+Definition foo (l : list nat) :=
+ match l with
+ | a :: (b :: l) as l1 => l1
+ | _ => l
+end.
+Print foo.
+End Issue7110.
+
+Module LocateNotations.
+Locate "exists".
+Locate "( _ , _ , .. , _ )".
+End LocateNotations.
diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out
new file mode 100644
index 0000000000..e9c28faf1d
--- /dev/null
+++ b/test-suite/output/Projections.out
@@ -0,0 +1,2 @@
+fun S : store => S.(store_funcs)
+ : store -> host_func
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
new file mode 100644
index 0000000000..098a518dc4
--- /dev/null
+++ b/test-suite/output/Projections.v
@@ -0,0 +1,11 @@
+
+Set Printing Projections.
+
+Class HostFunction := host_func : Type.
+
+Section store.
+ Context `{HostFunction}.
+ Record store := { store_funcs : host_func }.
+End store.
+
+Check (fun (S:@store nat) => S.(store_funcs)).
diff --git a/test-suite/output/UnclosedBlocks.out b/test-suite/output/UnclosedBlocks.out
index b83e94ad43..31481e84a5 100644
--- a/test-suite/output/UnclosedBlocks.out
+++ b/test-suite/output/UnclosedBlocks.out
@@ -1,3 +1,2 @@
-
Error: The section Baz, module type Bar and module Foo need to be closed.
diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out
index 91ceb1b583..d6056c5098 100644
--- a/test-suite/output/bug5778.out
+++ b/test-suite/output/bug5778.out
@@ -1,4 +1,4 @@
The command has indeed failed with message:
-In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call
-failed.
+In nested Ltac calls to "c", "abs", "abstract b ltac:(())",
+"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed.
The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug6404.out b/test-suite/output/bug6404.out
new file mode 100644
index 0000000000..05464755f0
--- /dev/null
+++ b/test-suite/output/bug6404.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+In nested Ltac calls to "c", "abs", "transparent_abstract (tactic3)",
+"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed.
+The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v
new file mode 100644
index 0000000000..bbe6b1a00f
--- /dev/null
+++ b/test-suite/output/bug6404.v
@@ -0,0 +1,7 @@
+Ltac a _ := pose (I : I).
+Ltac b _ := a ().
+Ltac abs _ := transparent_abstract b ().
+Ltac c _ := abs ().
+Goal True.
+ Fail c ().
+Abort.
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 6adbe95dd5..901b1e3aa6 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -37,17 +37,20 @@ Fail g1 I.
Fail f1 I.
Fail g2 I.
Fail f2 I.
+Abort.
Ltac h x := injection x.
Goal True -> False.
Fail h I.
intro H.
Fail h H.
+Abort.
(* Check printing of the "var" argument "Hx" *)
Ltac m H := idtac H; exact H.
Goal True.
let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
+Abort.
(* Check consistency of interpretation scopes (#4398) *)
diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out
new file mode 100644
index 0000000000..1515954060
--- /dev/null
+++ b/test-suite/output/ssr_clear.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Ltac call to "move (ssrmovearg) (ssrclauses)" failed.
+No assumption is named NO_SUCH_NAME
diff --git a/test-suite/output/ssr_clear.v b/test-suite/output/ssr_clear.v
new file mode 100644
index 0000000000..573ec47e0b
--- /dev/null
+++ b/test-suite/output/ssr_clear.v
@@ -0,0 +1,6 @@
+Require Import ssreflect.
+
+Example foo : True -> True.
+Proof.
+Fail move=> {NO_SUCH_NAME}.
+Abort.
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
new file mode 100644
index 0000000000..fa2393b910
--- /dev/null
+++ b/test-suite/output/ssr_explain_match.out
@@ -0,0 +1,55 @@
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ - _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ <= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ < _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ >= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ > _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ <= _ <= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ < _ <= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ <= _ < _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ < _ < _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ + _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ * _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+BEGIN INSTANCES
+instance: (x + y + z) matches: (x + y + z)
+instance: (x + y) matches: (x + y)
+instance: (x + y) matches: (x + y)
+END INSTANCES
+BEGIN INSTANCES
+instance: (addnC (x + y) z) matches: (x + y + z)
+instance: (addnC x y) matches: (x + y)
+instance: (addnC x y) matches: (x + y)
+END INSTANCES
+BEGIN INSTANCES
+instance: (addnA x y z) matches: (x + y + z)
+END INSTANCES
+BEGIN INSTANCES
+instance: (addnA x y z) matches: (x + y + z)
+instance: (addnC z (x + y)) matches: (x + y + z)
+instance: (addnC y x) matches: (x + y)
+instance: (addnC y x) matches: (x + y)
+END INSTANCES
+The command has indeed failed with message:
+Ltac call to "ssrinstancesoftpat (cpattern)" failed.
+Not supported
diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v
new file mode 100644
index 0000000000..56ca24b6e2
--- /dev/null
+++ b/test-suite/output/ssr_explain_match.v
@@ -0,0 +1,23 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+Require Import ssrmatching.
+Require Import ssreflect ssrbool TestSuite.ssr_mini_mathcomp.
+
+Definition addnAC := (addnA, addnC).
+
+Lemma test x y z : x + y + z = x + y.
+
+ssrinstancesoftpat (_ + _).
+ssrinstancesofruleL2R addnC.
+ssrinstancesofruleR2L addnA.
+ssrinstancesofruleR2L addnAC.
+Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *)
+Admitted.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 19:10:05 +0000