aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/output')
-rw-r--r--test-suite/output/MExtraction.v5
-rw-r--r--test-suite/output/PrintCanonicalProjections.out18
-rw-r--r--test-suite/output/PrintCanonicalProjections.v46
-rw-r--r--test-suite/output/print_ltac.out8
-rw-r--r--test-suite/output/print_ltac.v12
-rw-r--r--test-suite/output/relaxed_ambiguous_paths.out24
-rw-r--r--test-suite/output/relaxed_ambiguous_paths.v51
-rw-r--r--test-suite/output/unification.out11
-rw-r--r--test-suite/output/unification.v12
9 files changed, 174 insertions, 13 deletions
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index 668be1fdbc..357afb51eb 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -56,10 +56,11 @@ Extract Constant Rinv => "fun x -> 1 / x".
Recursive Extraction
Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
Tauto.abst_form
- ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ
+ ZMicromega.cnfZ ZMicromega.Zeval_const QMicromega.cnfQ
List.map simpl_cone (*map_cone indexes*)
denorm Qpower vm_add
normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+
(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)
diff --git a/test-suite/output/PrintCanonicalProjections.out b/test-suite/output/PrintCanonicalProjections.out
new file mode 100644
index 0000000000..a4e2251440
--- /dev/null
+++ b/test-suite/output/PrintCanonicalProjections.out
@@ -0,0 +1,18 @@
+bool <- sort_eq ( bool_eqType )
+bool <- sort_TYPE ( bool_TYPE )
+nat <- sort_eq ( nat_eqType )
+nat <- sort_TYPE ( nat_TYPE )
+prod <- sort_eq ( prod_eqType )
+prod <- sort_TYPE ( prod_TYPE )
+sum <- sort_eq ( sum_eqType )
+sum <- sort_TYPE ( sum_TYPE )
+sum <- sort_TYPE ( sum_TYPE )
+prod <- sort_TYPE ( prod_TYPE )
+nat <- sort_TYPE ( nat_TYPE )
+bool <- sort_TYPE ( bool_TYPE )
+sum <- sort_eq ( sum_eqType )
+prod <- sort_eq ( prod_eqType )
+nat <- sort_eq ( nat_eqType )
+bool <- sort_eq ( bool_eqType )
+bool <- sort_TYPE ( bool_TYPE )
+bool <- sort_eq ( bool_eqType )
diff --git a/test-suite/output/PrintCanonicalProjections.v b/test-suite/output/PrintCanonicalProjections.v
new file mode 100644
index 0000000000..808cdffe39
--- /dev/null
+++ b/test-suite/output/PrintCanonicalProjections.v
@@ -0,0 +1,46 @@
+Record TYPE := Pack_TYPE { sort_TYPE :> Type }.
+Record eqType := Pack_eq { sort_eq :> Type; _ : sort_eq -> sort_eq -> bool }.
+
+Definition eq_op (T : eqType) : T -> T -> bool :=
+ match T with Pack_eq _ op => op end.
+
+Definition bool_eqb b1 b2 :=
+ match b1, b2 with
+ | false, false => true
+ | true, true => true
+ | _, _ => false
+ end.
+
+Canonical bool_TYPE := Pack_TYPE bool.
+Canonical bool_eqType := Pack_eq bool bool_eqb.
+
+Canonical nat_TYPE := Pack_TYPE nat.
+Canonical nat_eqType := Pack_eq nat Nat.eqb.
+
+Definition prod_eqb (T U : eqType) (x y : T * U) :=
+ match x, y with
+ | (x1, x2), (y1, y2) =>
+ andb (eq_op _ x1 y1) (eq_op _ x2 y2)
+ end.
+
+Canonical prod_TYPE (T U : TYPE) := Pack_TYPE (T * U).
+Canonical prod_eqType (T U : eqType) := Pack_eq (T * U) (prod_eqb T U).
+
+Definition sum_eqb (T U : eqType) (x y : T + U) :=
+ match x, y with
+ | inl x, inl y => eq_op _ x y
+ | inr x, inr y => eq_op _ x y
+ | _, _ => false
+ end.
+
+Canonical sum_TYPE (T U : TYPE) := Pack_TYPE (T + U).
+Canonical sum_eqType (T U : eqType) := Pack_eq (T + U) (sum_eqb T U).
+
+Print Canonical Projections bool.
+Print Canonical Projections nat.
+Print Canonical Projections prod.
+Print Canonical Projections sum.
+Print Canonical Projections sort_TYPE.
+Print Canonical Projections sort_eq.
+Print Canonical Projections sort_TYPE bool.
+Print Canonical Projections bool_eqType.
diff --git a/test-suite/output/print_ltac.out b/test-suite/output/print_ltac.out
new file mode 100644
index 0000000000..952761acca
--- /dev/null
+++ b/test-suite/output/print_ltac.out
@@ -0,0 +1,8 @@
+Ltac t1 := time "my tactic" idtac
+Ltac t2 := let x := string:("my tactic") in
+ idtac
+ x
+Ltac t3 := idtacstr "my tactic"
+Ltac t4 x := match x with
+ | ?A => (A, A)
+ end
diff --git a/test-suite/output/print_ltac.v b/test-suite/output/print_ltac.v
new file mode 100644
index 0000000000..a992846791
--- /dev/null
+++ b/test-suite/output/print_ltac.v
@@ -0,0 +1,12 @@
+(* Testing of various things about Print Ltac *)
+(* https://github.com/coq/coq/issues/10971 *)
+Ltac t1 := time "my tactic" idtac.
+Print Ltac t1.
+Ltac t2 := let x := string:("my tactic") in idtac x.
+Print Ltac t2.
+Tactic Notation "idtacstr" string(str) := idtac str.
+Ltac t3 := idtacstr "my tactic".
+Print Ltac t3.
+(* https://github.com/coq/coq/issues/9716 *)
+Ltac t4 x := match x with ?A => constr:((A, A)) end.
+Print Ltac t4.
diff --git a/test-suite/output/relaxed_ambiguous_paths.out b/test-suite/output/relaxed_ambiguous_paths.out
index dc793598a9..ac5a09bad7 100644
--- a/test-suite/output/relaxed_ambiguous_paths.out
+++ b/test-suite/output/relaxed_ambiguous_paths.out
@@ -7,6 +7,16 @@ New coercion path [ac; cd] : A >-> D is ambiguous with existing
[ac] : A >-> C
[bd] : B >-> D
[cd] : C >-> D
+File "stdin", line 26, characters 0-28:
+Warning:
+New coercion path [ab; bc] : A >-> C is ambiguous with existing
+[ac] : A >-> C. [ambiguous-paths,typechecker]
+[ac] : A >-> C
+[ac; cd] : A >-> D
+[ab] : A >-> B
+[cd] : C >-> D
+[bc] : B >-> C
+[bc; cd] : B >-> D
[B_A] : B >-> A
[C_A] : C >-> A
[D_B] : D >-> B
@@ -21,7 +31,7 @@ New coercion path [ac; cd] : A >-> D is ambiguous with existing
[D_A] : D >-> A
[D_B] : D >-> B
[D_C] : D >-> C
-File "stdin", line 103, characters 0-86:
+File "stdin", line 121, characters 0-86:
Warning:
New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
[D_B; B_A'] : D >-> A'. [ambiguous-paths,typechecker]
@@ -34,3 +44,15 @@ New coercion path [D_C; C_A'] : D >-> A' is ambiguous with existing
[D_A] : D >-> A
[D_B] : D >-> B
[D_C] : D >-> C
+File "stdin", line 130, characters 0-47:
+Warning:
+New coercion path [unwrap_nat; wrap_nat] : NAT >-> NAT is not definitionally an identity function.
+[ambiguous-paths,typechecker]
+File "stdin", line 131, characters 0-64:
+Warning:
+New coercion path [unwrap_list; wrap_list] : LIST >-> LIST is not definitionally an identity function.
+[ambiguous-paths,typechecker]
+File "stdin", line 132, characters 0-51:
+Warning:
+New coercion path [unwrap_Type; wrap_Type] : TYPE >-> TYPE is not definitionally an identity function.
+[ambiguous-paths,typechecker]
diff --git a/test-suite/output/relaxed_ambiguous_paths.v b/test-suite/output/relaxed_ambiguous_paths.v
index a4af27539c..41322045f2 100644
--- a/test-suite/output/relaxed_ambiguous_paths.v
+++ b/test-suite/output/relaxed_ambiguous_paths.v
@@ -16,6 +16,24 @@ End test1.
Module test2.
Section test2.
+
+Variable (A B C D : Type).
+Variable (ab : A -> B) (bc : B -> C) (ac : A -> C) (cd : C -> D).
+
+Local Coercion ac : A >-> C.
+Local Coercion cd : C >-> D.
+Local Coercion ab : A >-> B.
+Local Coercion bc : B >-> C.
+(* `[ab; bc; cd], [ac; cd] : A >-> D` should not be shown as ambiguous paths *)
+(* here because they are redundant with `[ab; bc], [ac] : A >-> C`. *)
+
+Print Graph.
+
+End test2.
+End test2.
+
+Module test3.
+Section test3.
Variable (A : Type) (P Q : A -> Prop).
Record B := {
@@ -39,11 +57,11 @@ Local Coercion D_C (d : D) : C := Build_C (D_A d) (D_Q d).
Print Graph.
-End test2.
-End test2.
+End test3.
+End test3.
-Module test3.
-Section test3.
+Module test4.
+Section test4.
Variable (A : Type) (P Q : A -> Prop).
@@ -71,11 +89,11 @@ Local Coercion D_C (d : D) : C true := Build_C true (D_A d) (D_Q d).
Print Graph.
-End test3.
-End test3.
+End test4.
+End test4.
-Module test4.
-Section test4.
+Module test5.
+Section test5.
Variable (A : Type) (P Q : A -> Prop).
@@ -105,5 +123,18 @@ Local Coercion D_C (d : D) : C true :=
Print Graph.
-End test4.
-End test4.
+End test5.
+End test5.
+
+Module test6.
+Record > NAT := wrap_nat { unwrap_nat :> nat }.
+Record > LIST (T : Type) := wrap_list { unwrap_list :> list T }.
+Record > TYPE := wrap_Type { unwrap_Type :> Type }.
+End test6.
+
+Module test7.
+Set Primitive Projections.
+Record > NAT_prim := wrap_nat { unwrap_nat :> nat }.
+Record > LIST_prim (T : Type) := wrap_list { unwrap_list :> list T }.
+Record > TYPE_prim := wrap_Type { unwrap_Type :> Type }.
+End test7.
diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out
new file mode 100644
index 0000000000..dfd755da61
--- /dev/null
+++ b/test-suite/output/unification.out
@@ -0,0 +1,11 @@
+The command has indeed failed with message:
+In environment
+x : T
+T : Type
+a : T
+Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate
+"?X" because "T" is not in its scope: available arguments are
+"x" "C a").
+The command has indeed failed with message:
+The term "id" has type "ID" while it is expected to have type
+"Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope).
diff --git a/test-suite/output/unification.v b/test-suite/output/unification.v
new file mode 100644
index 0000000000..ff99f2e23c
--- /dev/null
+++ b/test-suite/output/unification.v
@@ -0,0 +1,12 @@
+(* Unification error tests *)
+
+Module A.
+
+(* Check regression of an UNBOUND_REL bug *)
+Inductive T := C : forall {A}, A -> T.
+Fail Check fun x => match x return ?[X] with C a => a end.
+
+(* Bug #3634 *)
+Fail Check (id:Type -> _).
+
+End A.
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:42:27 +0000