aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/README.md22
-rw-r--r--test-suite/bugs/closed/2800.v13
-rw-r--r--test-suite/bugs/closed/5500.v35
-rw-r--r--test-suite/bugs/closed/5547.v16
-rw-r--r--test-suite/bugs/closed/7421.v39
-rw-r--r--test-suite/bugs/closed/7615.v19
-rw-r--r--test-suite/bugs/closed/7700.v9
-rw-r--r--test-suite/bugs/closed/7779.v15
-rw-r--r--test-suite/bugs/closed/7780.v16
-rw-r--r--test-suite/bugs/closed/7811.v114
-rw-r--r--test-suite/output/PrintAssumptions.out2
-rw-r--r--test-suite/output/PrintAssumptions.v27
-rw-r--r--test-suite/output/Unicode.out41
-rw-r--r--test-suite/output/Unicode.v28
-rw-r--r--test-suite/ssr/ipat_clear_if_id.v23
-rw-r--r--test-suite/ssr/rew_polyuniv.v90
-rw-r--r--test-suite/ssr/set_polyuniv.v11
-rw-r--r--test-suite/ssr/ssr_rew_illtyped.v9
-rw-r--r--test-suite/success/Hints.v2
-rw-r--r--test-suite/success/letproj.v2
-rw-r--r--test-suite/success/primitiveproj.v21
21 files changed, 545 insertions, 9 deletions
diff --git a/test-suite/README.md b/test-suite/README.md
index ef2e574ec..e81da0830 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -62,20 +62,26 @@ BUILDING SUMMARY FILE
NO FAILURES
```
-See [`test-suite/Makefile`](/test-suite/Makefile) for more information.
+See [`test-suite/Makefile`](Makefile) for more information.
## Adding a test
-Regression tests for closed bugs should be added to `test-suite/bugs/closed`, as `1234.v` where `1234` is the bug number.
+Regression tests for closed bugs should be added to
+[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number.
Files in this directory are tested for successful compilation.
When you fix a bug, you should usually add a regression test here as well.
-The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile.
+The error "(bug seems to be opened, please check)" when running
+`make test-suite` means that a test in [`bugs/closed`](bugs/closed) failed to
+compile.
-There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output.
+There are also output tests in [`output`](output) which consist of a `.v` file
+and a `.out` file with the expected output.
-There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit`
-unit-test framework, as described at http://ounit.forge.ocamlcore.org/. Use `make unit-tests' in the unit-tests directory to run them.
+There are unit tests of OCaml code in [`unit-tests`](unit-tests). These tests
+are contained in `.ml` files, and rely on the `OUnit` unit-test framework, as
+described at <http://ounit.forge.ocamlcore.org/>. Use `make unit-tests` in the
+[`unit-tests`](unit-tests) directory to run them.
## Fixing output tests
@@ -88,5 +94,5 @@ automatically.
Don't forget to check the updated `.out` files into git!
Note that `output/MExtraction.out` is special: it is copied from
-`micromega/micromega.ml` in the plugin source directory. Automatic
-approval will incorrectly update the copy.
+[`micromega/micromega.ml`](../plugins/micromega/micromega.ml) in the plugin
+source directory. Automatic approval will incorrectly update the copy.
diff --git a/test-suite/bugs/closed/2800.v b/test-suite/bugs/closed/2800.v
index 2ee438934..54c75e344 100644
--- a/test-suite/bugs/closed/2800.v
+++ b/test-suite/bugs/closed/2800.v
@@ -4,3 +4,16 @@ intuition
match goal with
| |- _ => idtac " foo"
end.
+
+ lazymatch goal with _ => idtac end.
+ match goal with _ => idtac end.
+ unshelve lazymatch goal with _ => idtac end.
+ unshelve match goal with _ => idtac end.
+ unshelve (let x := I in idtac).
+Abort.
+
+Require Import ssreflect.
+
+Goal True.
+match goal with _ => idtac end => //.
+Qed.
diff --git a/test-suite/bugs/closed/5500.v b/test-suite/bugs/closed/5500.v
new file mode 100644
index 000000000..aa63e2ab0
--- /dev/null
+++ b/test-suite/bugs/closed/5500.v
@@ -0,0 +1,35 @@
+(* Too weak check on the correctness of return clause was leading to an anomaly *)
+
+Inductive Vector A: nat -> Type :=
+ nil: Vector A O
+| cons: forall n, A -> Vector A n -> Vector A (S n).
+
+(* This could be made working with a better inference of inner return
+ predicates from the return predicate at the higher level of the
+ nested matching. Currently, we only check that it does not raise an
+ anomaly, but eventually, the "Fail" could be removed. *)
+
+Fail Definition hd_fst A x n (v: A * Vector A (S n)) :=
+ match v as v0 return match v0 with
+ (l, r) =>
+ match r in Vector _ n return match n with 0 => Type | S _ => Type end with
+ nil _ => A
+ | cons _ _ _ _ => A
+ end
+ end with
+ (_, nil _) => x
+ | (_, cons _ n hd tl) => hd
+ end.
+
+(* This is another example of failure but involving beta-reduction and
+ not iota-reduction. Thus, for this one, I don't see how it could be
+ solved by small inversion, whatever smart is small inversion. *)
+
+Inductive A : (Type->Type) -> Type := J : A (fun x => x).
+
+Fail Check fun x : nat * A (fun x => x) =>
+ match x return match x with
+ (y,z) => match z in A f return f Type with J => bool end
+ end with
+ (y,J) => true
+ end.
diff --git a/test-suite/bugs/closed/5547.v b/test-suite/bugs/closed/5547.v
new file mode 100644
index 000000000..79633f489
--- /dev/null
+++ b/test-suite/bugs/closed/5547.v
@@ -0,0 +1,16 @@
+(* Checking typability of intermediate return predicates in nested pattern-matching *)
+
+Inductive A : (Type->Type) -> Type := J : A (fun x => x).
+Definition ret (x : nat * A (fun x => x))
+ := match x return Type with
+ | (y,z) => match z in A f return f Type with
+ | J => bool
+ end
+ end.
+Definition foo : forall x, ret x.
+Proof.
+Fail refine (fun x
+ => match x return ret x with
+ | (y,J) => true
+ end
+ ).
diff --git a/test-suite/bugs/closed/7421.v b/test-suite/bugs/closed/7421.v
new file mode 100644
index 000000000..afcdd35fc
--- /dev/null
+++ b/test-suite/bugs/closed/7421.v
@@ -0,0 +1,39 @@
+
+
+Universe i j.
+
+Goal False.
+Proof.
+ Check Type@{i} : Type@{j}.
+ Fail constr_eq_strict Type@{i} Type@{j}.
+ assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *)
+ Fail constr_eq_strict Type@{i} Type@{j}.
+
+ constr_eq Type@{i} Type@{j}. (* <- i=j is retained *)
+ constr_eq_strict Type@{i} Type@{j}.
+ Fail Check Type@{i} : Type@{j}.
+
+ Fail constr_eq Prop Set.
+ Fail constr_eq Prop Type.
+
+ Fail constr_eq_strict Type Type.
+ constr_eq Type Type.
+
+ constr_eq_strict Set Set.
+ constr_eq Set Set.
+ constr_eq Prop Prop.
+
+ let x := constr:(Type) in constr_eq_strict x x.
+ let x := constr:(Type) in constr_eq x x.
+
+ Fail lazymatch type of prod with
+ | ?A -> ?B -> _ => constr_eq_strict A B
+ end.
+ lazymatch type of prod with
+ | ?A -> ?B -> _ => constr_eq A B
+ end.
+ lazymatch type of prod with
+ | ?A -> ?B -> ?C => constr_eq A C
+ end.
+
+Abort.
diff --git a/test-suite/bugs/closed/7615.v b/test-suite/bugs/closed/7615.v
new file mode 100644
index 000000000..cd8c4ad7d
--- /dev/null
+++ b/test-suite/bugs/closed/7615.v
@@ -0,0 +1,19 @@
+Set Universe Polymorphism.
+
+Module Type S.
+Parameter Inline T@{i} : Type@{i+1}.
+End S.
+
+Module F (X : S).
+Definition X@{j i} : Type@{j} := X.T@{i}.
+End F.
+
+Module M.
+Definition T@{i} := Type@{i}.
+End M.
+
+Module N := F(M).
+
+Require Import Hurkens.
+
+Fail Definition eqU@{i j} : @eq Type@{j} N.X@{i Set} Type@{i} := eq_refl.
diff --git a/test-suite/bugs/closed/7700.v b/test-suite/bugs/closed/7700.v
new file mode 100644
index 000000000..56f5481ba
--- /dev/null
+++ b/test-suite/bugs/closed/7700.v
@@ -0,0 +1,9 @@
+(* Abbreviations to section variables were not located *)
+Section foo.
+ Let x := Set.
+ Notation y := x.
+ Check y.
+ Variable x' : Set.
+ Notation y' := x'.
+ Check y'.
+End foo.
diff --git a/test-suite/bugs/closed/7779.v b/test-suite/bugs/closed/7779.v
new file mode 100644
index 000000000..78936b595
--- /dev/null
+++ b/test-suite/bugs/closed/7779.v
@@ -0,0 +1,15 @@
+(* Checking that the "in" clause takes the "eqn" clause into account *)
+
+Definition test (x: nat): {y: nat | False }. Admitted.
+
+Parameter x: nat.
+Parameter z: nat.
+
+Goal
+ proj1_sig (test x) = z ->
+ False.
+Proof.
+ intro H.
+ destruct (test x) eqn:Heqs in H.
+ change (test x = exist (fun _ : nat => False) x0 f) in Heqs. (* Check it has the expected statement *)
+Abort.
diff --git a/test-suite/bugs/closed/7780.v b/test-suite/bugs/closed/7780.v
new file mode 100644
index 000000000..2318f4d6e
--- /dev/null
+++ b/test-suite/bugs/closed/7780.v
@@ -0,0 +1,16 @@
+(* A lift was missing in expanding aliases under binders for unification *)
+
+(* Below, the lift was missing while expanding the reference to
+ [mkcons] in [?N] which was under binder [arg] *)
+
+Goal forall T (t : T) (P P0 : T -> Set), option (option (list (P0 t)) -> option (list (P t))).
+ intros ????.
+ refine (Some
+ (fun rls
+ => let mkcons := ?[M] in
+ let default arg := ?[N] in
+ match rls as rls (* 2 *) return option (list (P ?[O])) with
+ | Some _ => None
+ | None => None
+ end)).
+Abort.
diff --git a/test-suite/bugs/closed/7811.v b/test-suite/bugs/closed/7811.v
new file mode 100644
index 000000000..fee330f22
--- /dev/null
+++ b/test-suite/bugs/closed/7811.v
@@ -0,0 +1,114 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 140 lines to 26 lines, then from 141 lines to 27 lines, then from 142 lines to 27 lines, then from 272 lines to 61 lines, then from 291 lines to 94 lines, then from 678 lines to 142 lines, then from 418 lines to 161 lines, then from 538 lines to 189 lines, then from 840 lines to 493 lines, then from 751 lines to 567 lines, then from 913 lines to 649 lines, then from 875 lines to 666 lines, then from 784 lines to 568 lines, then from 655 lines to 173 lines, then from 317 lines to 94 lines, then from 172 lines to 86 lines, then from 102 lines to 86 lines, then from 130 lines to 86 lines, then from 332 lines to 112 lines, then from 279 lines to 111 lines, then from 3996 lines to 5697 lines, then from 153 lines to 117 lines, then from 146 lines to 108 lines, then from 124 lines to 108 lines *)
+(* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3
+ coqtop version 8.8.0 (May 2018) *)
+
+(* This was triggering a "Not_found" at the time of printing/showing the goal *)
+
+Require Coq.Unicode.Utf8.
+
+Notation "t $ r" := (t r)
+ (at level 65, right associativity, only parsing).
+
+Inductive tele : Type :=
+ | TeleO : tele
+ | TeleS {X} (binder : X -> tele) : tele.
+
+Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
+ match TT with
+ | TeleO => T
+ | TeleS b => forall x, tele_fun (b x) T
+ end.
+
+Inductive tele_arg : tele -> Type :=
+| TargO : tele_arg TeleO
+| TargS {X} {binder} (x : X) : tele_arg (binder x) -> tele_arg (TeleS binder).
+
+Axiom tele_app : forall {TT : tele} {T} (f : tele_fun TT T), tele_arg TT -> T.
+
+Coercion tele_arg : tele >-> Sortclass.
+
+Inductive val :=
+ | LitV
+ | PairV (v1 v2 : val)
+ | InjLV (v : val)
+ | InjRV (v : val).
+Axiom coPset : Set.
+Axiom atomic_update : forall {PROP : Type} {TA TB : tele}, coPset -> coPset -> (TA -> PROP) -> (TA -> TB -> PROP) -> (TA -> TB -> PROP) -> PROP.
+Import Coq.Unicode.Utf8.
+Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
+ (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. ))
+ (TB:=TeleO)
+ Eo Ei
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, α) ..)
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, tele_app (TT:=TeleO) β) .. )
+ (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $
+ λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ) .. )
+ )
+ (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder,
+ format "'[ ' 'AU' '<<' ∀ x1 .. xn , α '>>' '/' @ Eo , Ei '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope.
+
+Axiom ident : Set.
+Inductive env (A : Type) : Type := Enil : env A | Esnoc : env A → ident → A → env A.
+Record envs (PROP : Type) : Type
+ := Envs { env_spatial : env PROP }.
+Axiom positive : Set.
+Axiom Qp : Set.
+Axiom one : positive.
+Goal forall (T : Type) (T0 : forall _ : T, Type) (P : Set)
+ (u : T) (γs : P) (Q : T0 u) (Φ o : forall _ : val, T0 u)
+ (stack_content0 : forall (_ : P) (_ : list val), T0 u)
+ (c c0 : coPset) (l : forall (A : Type) (_ : list A), list A)
+ (e0 : forall (_ : env (T0 u)) (_ : positive), envs (T0 u))
+ (i0 : ident) (o1 : forall (_ : Qp) (_ : val), T0 u)
+ (b0 : forall _ : env (T0 u), T0 u) (P0 : forall _ : T0 u, Type)
+ (u0 : forall (_ : T0 u) (_ : T0 u), T0 u),
+ P0
+ (@atomic_update (T0 u)
+ (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO))) TeleO c c0
+ (@tele_app (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO)))
+ (T0 u) (fun (v : val) (q : Qp) => o1 q v))
+ (@tele_app (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO)))
+ (forall _ : tele_arg TeleO, T0 u)
+ (fun (v : val) (q : Qp) => @tele_app TeleO (T0 u) (o1 q v)))
+ (@tele_app (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO)))
+ (forall _ : tele_arg TeleO, T0 u)
+ (fun (x : val) (_ : Qp) =>
+ @tele_app TeleO (T0 u)
+ (u0
+ (b0
+ match
+ e0
+ (@Esnoc (T0 u) (@Enil (T0 u)) i0
+ (@atomic_update (T0 u)
+ (@TeleS (list val) (fun _ : list val => TeleO)) TeleO
+ c c0
+ (@tele_app
+ (@TeleS (list val) (fun _ : list val => TeleO))
+ (T0 u) (fun l0 : list val => stack_content0 γs l0))
+ (@tele_app
+ (@TeleS (list val) (fun _ : list val => TeleO))
+ (forall _ : tele_arg TeleO, T0 u)
+ (fun l0 : list val =>
+ @tele_app TeleO (T0 u)
+ (stack_content0 γs (l val l0))))
+ (@tele_app
+ (@TeleS (list val) (fun _ : list val => TeleO))
+ (forall _ : tele_arg TeleO, T0 u)
+ (fun x1 : list val =>
+ @tele_app TeleO (T0 u)
+ (u0 Q
+ (Φ
+ match x1 return val with
+ | nil => InjLV LitV
+ | cons v _ => InjRV v
+ end)))))) one
+ return (env (T0 u))
+ with
+ | Envs _ env_spatial0 => env_spatial0
+ end) (o x)))))
+.
+ Show.
+Abort.
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index 66458543a..34f44cd24 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/test-suite/output/PrintAssumptions.out
@@ -18,3 +18,5 @@ Closed under the global context
Closed under the global context
Axioms:
M.foo : False
+Closed under the global context
+Closed under the global context
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
index c2003816c..ea1ab6378 100644
--- a/test-suite/output/PrintAssumptions.v
+++ b/test-suite/output/PrintAssumptions.v
@@ -110,3 +110,30 @@ End N.
Print Assumptions N.foo.
End INCLUDE.
+
+(* Print Assumptions did not enter implementation of submodules (#7192) *)
+
+Module SUBMODULES.
+
+Definition a := True.
+Module Type B. Axiom f : Prop. End B.
+Module Type C. Declare Module D : B. End C.
+Module E: C.
+ Module D <: B. Definition f := a. End D.
+End E.
+Print Assumptions E.D.f.
+
+(* Idem in the scope of a functor *)
+
+Module Type T. End T.
+Module F (X : T).
+ Definition a := True.
+ Module Type B. Axiom f : Prop. End B.
+ Module Type C. Declare Module D : B. End C.
+ Module E: C.
+ Module D <: B. Definition f := a. End D.
+ End E.
+ Print Assumptions E.D.f.
+End F.
+
+End SUBMODULES.
diff --git a/test-suite/output/Unicode.out b/test-suite/output/Unicode.out
new file mode 100644
index 000000000..a57b3bbad
--- /dev/null
+++ b/test-suite/output/Unicode.out
@@ -0,0 +1,41 @@
+1 subgoal
+
+ very_very_long_type_name1 : Type
+ very_very_long_type_name2 : Type
+ f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+ ============================
+ True
+ → True
+ → ∀ (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y
+1 subgoal
+
+ very_very_long_type_name1 : Type
+ very_very_long_type_name2 : Type
+ f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+ ============================
+ True
+ → True
+ → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1)
+ (z : very_very_long_type_name2), f y x ∧ f y z
+1 subgoal
+
+ very_very_long_type_name1 : Type
+ very_very_long_type_name2 : Type
+ f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+ ============================
+ True
+ → True
+ → ∀ (x : very_very_long_type_name2) (y : very_very_long_type_name1)
+ (z : very_very_long_type_name2),
+ f y x ∧ f y z ∧ f y x ∧ f y z ∧ f y x ∧ f y z
+1 subgoal
+
+ very_very_long_type_name1 : Type
+ very_very_long_type_name2 : Type
+ f : very_very_long_type_name1 → very_very_long_type_name2 → Prop
+ ============================
+ True
+ → True
+ → ∃ (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y ∧ f x y
diff --git a/test-suite/output/Unicode.v b/test-suite/output/Unicode.v
new file mode 100644
index 000000000..42b07e5a0
--- /dev/null
+++ b/test-suite/output/Unicode.v
@@ -0,0 +1,28 @@
+Require Import Coq.Unicode.Utf8.
+
+Section test.
+Context (very_very_long_type_name1 : Type) (very_very_long_type_name2 : Type).
+Context (f : very_very_long_type_name1 -> very_very_long_type_name2 -> Prop).
+
+Lemma test : True -> True ->
+ forall (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+ f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
+Proof. Show. Abort.
+
+Lemma test : True -> True ->
+ forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
+ (z : very_very_long_type_name2),
+ f y x /\ f y z.
+Proof. Show. Abort.
+
+Lemma test : True -> True ->
+ forall (x : very_very_long_type_name2) (y : very_very_long_type_name1)
+ (z : very_very_long_type_name2),
+ f y x /\ f y z /\ f y x /\ f y z /\ f y x /\ f y z.
+Proof. Show. Abort.
+
+Lemma test : True -> True ->
+ exists (x : very_very_long_type_name1) (y : very_very_long_type_name2),
+ f x y /\ f x y /\ f x y /\ f x y /\ f x y /\ f x y.
+Proof. Show. Abort.
+End test.
diff --git a/test-suite/ssr/ipat_clear_if_id.v b/test-suite/ssr/ipat_clear_if_id.v
new file mode 100644
index 000000000..7a44db2ea
--- /dev/null
+++ b/test-suite/ssr/ipat_clear_if_id.v
@@ -0,0 +1,23 @@
+Require Import ssreflect.
+
+Axiom v1 : nat -> bool.
+
+Section Foo.
+
+Variable v2 : nat -> bool.
+
+Lemma test (v3 : nat -> bool) (v4 : bool -> bool) (v5 : bool -> bool) : nat -> nat -> nat -> nat -> True.
+Proof.
+move=> {}/v1 b1 {}/v2 b2 {}/v3 b3 {}/v2/v4/v5 b4.
+Check b1 : bool.
+Check b2 : bool.
+Check b3 : bool.
+Check b4 : bool.
+Fail Check v3.
+Fail Check v4.
+Fail Check v5.
+Check v2 : nat -> bool.
+by [].
+Qed.
+
+End Foo.
diff --git a/test-suite/ssr/rew_polyuniv.v b/test-suite/ssr/rew_polyuniv.v
new file mode 100644
index 000000000..e2bbbc9ec
--- /dev/null
+++ b/test-suite/ssr/rew_polyuniv.v
@@ -0,0 +1,90 @@
+From Coq Require Import Utf8 Setoid ssreflect.
+Set Default Proof Using "Type".
+
+Local Set Universe Polymorphism.
+
+(** Telescopes *)
+Inductive tele : Type :=
+ | TeleO : tele
+ | TeleS {X} (binder : X → tele) : tele.
+
+Arguments TeleS {_} _.
+
+(** The telescope version of Coq's function type *)
+Fixpoint tele_fun (TT : tele) (T : Type) : Type :=
+ match TT with
+ | TeleO => T
+ | TeleS b => ∀ x, tele_fun (b x) T
+ end.
+
+Notation "TT -t> A" :=
+ (tele_fun TT A) (at level 99, A at level 200, right associativity).
+
+(** A sigma-like type for an "element" of a telescope, i.e. the data it
+ takes to get a [T] from a [TT -t> T]. *)
+Inductive tele_arg : tele → Type :=
+| TargO : tele_arg TeleO
+(* the [x] is the only relevant data here *)
+| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder).
+
+Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T :=
+ λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T :=
+ match a in tele_arg TT return (TT -t> T) → T with
+ | TargO => λ t : T, t
+ | TargS x a => λ f, rec a (f x)
+ end) TT a f.
+Arguments tele_app {!_ _} _ !_ /.
+
+Coercion tele_arg : tele >-> Sortclass.
+Coercion tele_app : tele_fun >-> Funclass.
+
+(** Inversion lemma for [tele_arg] *)
+Lemma tele_arg_inv {TT : tele} (a : TT) :
+ match TT as TT return TT → Prop with
+ | TeleO => λ a, a = TargO
+ | TeleS f => λ a, ∃ x a', a = TargS x a'
+ end a.
+Proof. induction a; eauto. Qed.
+Lemma tele_arg_O_inv (a : TeleO) : a = TargO.
+Proof. exact (tele_arg_inv a). Qed.
+Lemma tele_arg_S_inv {X} {f : X → tele} (a : TeleS f) :
+ ∃ x a', a = TargS x a'.
+Proof. exact (tele_arg_inv a). Qed.
+
+(** Operate below [tele_fun]s with argument telescope [TT]. *)
+Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U :=
+ match TT as TT return (TT → U) → TT -t> U with
+ | TeleO => λ F, F TargO
+ | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *)
+ tele_bind (λ a, F (TargS x a))
+ end.
+Arguments tele_bind {_ !_} _ /.
+
+(* Show that tele_app ∘ tele_bind is the identity. *)
+Lemma tele_app_bind {U} {TT : tele} (f : TT → U) x :
+ (tele_app (tele_bind f)) x = f x.
+Proof.
+ induction TT as [|X b IH]; simpl in *.
+ - rewrite (tele_arg_O_inv x). auto.
+ - destruct (tele_arg_S_inv x) as [x' [a' ->]]. simpl.
+ rewrite IH. auto.
+Qed.
+
+(** Notation-compatible telescope mapping *)
+(* This adds (tele_app ∘ tele_bind), which is an identity function, around every
+ binder so that, after simplifying, this matches the way we typically write
+ notations involving telescopes. *)
+Notation "'λ..' x .. y , e" :=
+ (tele_app (tele_bind (λ x, .. (tele_app (tele_bind (λ y, e))) .. )))
+ (at level 200, x binder, y binder, right associativity,
+ format "'[ ' 'λ..' x .. y ']' , e").
+
+(* The testcase *)
+Lemma test {TA TB : tele} {X} (α' β' γ' : X → Prop) (Φ : TA → TB → Prop) x' :
+ (forall P Q, ((P /\ Q) = Q) * ((P -> Q) = Q)) ->
+ ∀ a b, Φ a b = (λ.. x y, β' x' ∧ (γ' x' → Φ x y)) a b.
+Proof.
+intros cheat a b.
+rewrite !tele_app_bind.
+by rewrite !cheat.
+Qed.
diff --git a/test-suite/ssr/set_polyuniv.v b/test-suite/ssr/set_polyuniv.v
new file mode 100644
index 000000000..436eeafc7
--- /dev/null
+++ b/test-suite/ssr/set_polyuniv.v
@@ -0,0 +1,11 @@
+From Coq Require Import ssreflect.
+Set Default Proof Using "Type".
+
+Local Set Universe Polymorphism.
+
+Axiom foo : Type -> Prop.
+
+Lemma test : foo nat.
+Proof.
+set x := foo _. (* key @foo{i} matches @foo{j} *)
+Abort.
diff --git a/test-suite/ssr/ssr_rew_illtyped.v b/test-suite/ssr/ssr_rew_illtyped.v
new file mode 100644
index 000000000..7358068c8
--- /dev/null
+++ b/test-suite/ssr/ssr_rew_illtyped.v
@@ -0,0 +1,9 @@
+From Coq Require Import ssreflect Setoid.
+
+Structure SEProp := {prop_of : Prop; _ : prop_of <-> True}.
+
+Fact anomaly: forall P : SEProp, prop_of P.
+Proof.
+move=> [P E].
+Fail rewrite E.
+Abort.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 8d08f5975..717dc0deb 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -169,7 +169,7 @@ Proof.
Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e)
(a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances.
- Timeout 1 Fail apply _. (* 0.06s *)
+Timeout 1 Fail apply _. (* 0.06s *)
Abort.
End HintCut.
diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v
index de2857b43..2f0d8bf8c 100644
--- a/test-suite/success/letproj.v
+++ b/test-suite/success/letproj.v
@@ -7,3 +7,5 @@ Definition test (A : Type) (f : Foo A) :=
Scheme foo_case := Case for Foo Sort Type.
+Definition test' (A : Type) (f : Foo A) :=
+ let 'Build_Foo _ x y := f in x.
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 31a1608c4..7ca2767a5 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -199,3 +199,24 @@ split.
reflexivity.
Qed.
*)
+
+(* Primitive projection match compilation *)
+Require Import List.
+Set Primitive Projections.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+Arguments pair {_ _} _ _.
+
+Fixpoint split_at {A} (l : list A) (n : nat) : prod (list A) (list A) :=
+ match n with
+ | 0 => pair nil l
+ | S n =>
+ match l with
+ | nil => pair nil nil
+ | x :: l => let 'pair l1 l2 := split_at l n in pair (x :: l1) l2
+ end
+ end.
+
+Time Eval vm_compute in split_at (repeat 0 20) 10. (* Takes 0s *)
+Time Eval vm_compute in split_at (repeat 0 40) 20. (* Takes 0.001s *)
+Timeout 1 Time Eval vm_compute in split_at (repeat 0 60) 30. (* Used to take 60s, now takes 0.001s *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 04:18:47 +0000