From 4e70791036a1ab189579e109b428f46f45698b59 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 12:13:04 +0200
Subject: Adding a fold_glob_constr_with_binders combinator.

Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.

Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
---
 test-suite/success/boundvars.v | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 test-suite/success/boundvars.v

(limited to 'test-suite/success')

diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v
new file mode 100644
index 0000000000..7b6696af8e
--- /dev/null
+++ b/test-suite/success/boundvars.v
@@ -0,0 +1,5 @@
+(* An example showing a bug in the detection of free variables *)
+(* "x" is not free in the common type of "x" and "y" *)
+
+Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
+
-- 
cgit v1.2.3


From b4936da085b19ad508346d8e07ce1e922ef79c2d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 15:05:16 +0200
Subject: Using fold_glob_constr_with_binders to code bound_glob_vars.

To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.

This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
---
 test-suite/success/boundvars.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v
index 7b6696af8e..fafe272925 100644
--- a/test-suite/success/boundvars.v
+++ b/test-suite/success/boundvars.v
@@ -3,3 +3,12 @@
 
 Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
 
+(* An example showing a bug in the detection of bound variables *)
+
+Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl.
+intro.
+match goal with
+|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end.
+intro.
+Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *)
+Abort.
-- 
cgit v1.2.3


From 5f3d20dc53ffd0537a84c93acd761c3c69081342 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 10 Jun 2016 19:12:49 -0400
Subject: Add transparent_abstract tactic

---
 test-suite/success/transparent_abstract.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/success/transparent_abstract.v

(limited to 'test-suite/success')

diff --git a/test-suite/success/transparent_abstract.v b/test-suite/success/transparent_abstract.v
new file mode 100644
index 0000000000..ff4509c4a8
--- /dev/null
+++ b/test-suite/success/transparent_abstract.v
@@ -0,0 +1,21 @@
+Class by_transparent_abstract {T} (x : T) := make_by_transparent_abstract : T.
+Hint Extern 0 (@by_transparent_abstract ?T ?x) => change T; transparent_abstract exact_no_check x : typeclass_instances.
+
+Goal True /\ True.
+Proof.
+  split.
+  transparent_abstract exact I using foo.
+  let x := (eval hnf in foo) in constr_eq x I.
+  let x := constr:(ltac:(constructor) : True) in
+  let T := type of x in
+  let x := constr:(_ : by_transparent_abstract x) in
+  let x := (eval cbv delta [by_transparent_abstract] in (let y : T := x in y)) in
+  pose x as x'.
+  simpl in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then fail 0 else idtac.
+  hnf in x'.
+  let v := eval cbv [x'] in x' in tryif constr_eq v I then idtac else fail 0.
+  exact x'.
+Defined.
+Check eq_refl : I = foo.
+Eval compute in foo.
-- 
cgit v1.2.3


From 12f1c409daf2cdbd7d0323f0d61723819532b362 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 16:56:25 +0200
Subject: Really fixing #2602 which was wrongly working because of #5487 hiding
 the cause.

The cause was a missing evar/evar clause in ltac pattern-matching
function (constr_matching.ml).
---
 test-suite/success/ltac.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index ce90990594..d7ec092d76 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -317,3 +317,16 @@ let T := constr:(fun a b : nat => a) in
   end.
 exact (eq_refl n).
 Qed.
+
+(* A variant of #2602 which was wrongly succeeding because "a", bound to
+   "?m", was then internally turned into a "_" in the second matching *)
+
+Goal exists m, S m > 0.
+eexists.
+Fail match goal with
+ | |- context [ S ?a ] =>
+     match goal with
+       | |- S a > a => idtac
+     end
+end.
+Abort.
-- 
cgit v1.2.3


From f6856c5022ef27cdc492daadd1301cfcad025b01 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Mon, 1 May 2017 11:34:00 -0400
Subject: remove unneeded -emacs flag to coq-prog-args

---
 test-suite/success/Compat84.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite/success')

diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
index db6348fa17..732a024fc1 100644
--- a/test-suite/success/Compat84.v
+++ b/test-suite/success/Compat84.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
 
 Goal True.
   solve [ constructor 1 ]. Undo.
-- 
cgit v1.2.3


From cea40f37ab638031b9d5c6434ee5651a16ea1f3e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 09:04:17 +0200
Subject: Fixing Set Rewriting Schemes bugs introduced in v8.5.

- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
---
 test-suite/success/Scheme.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
index dd5aa81d1d..855f26698c 100644
--- a/test-suite/success/Scheme.v
+++ b/test-suite/success/Scheme.v
@@ -2,3 +2,26 @@
 
 Scheme Induction for eq Sort Prop.
 Check eq_ind_dep.
+
+(* This was broken in v8.5 *)
+
+Set Rewriting Schemes.
+Inductive myeq A (a:A) : A -> Prop := myrefl : myeq A a a.
+Unset Rewriting Schemes.
+
+Check myeq_rect.
+Check myeq_ind.
+Check myeq_rec.
+Check myeq_congr.
+Check myeq_sym_internal.
+Check myeq_rew.
+Check myeq_rew_dep.
+Check myeq_rew_fwd_dep.
+Check myeq_rew_r.
+Check internal_myeq_sym_involutive.
+Check myeq_rew_r_dep.
+Check myeq_rew_fwd_r_dep.
+
+Set Rewriting Schemes.
+Inductive myeq_true : bool -> Prop := myrefl_true : myeq_true true.
+Unset Rewriting Schemes.
-- 
cgit v1.2.3


From e9b745af47ba3386724b874e3fd74b6dad33b015 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Thu, 6 Apr 2017 22:48:32 +0200
Subject: Allow flexible anonymous universes in instances and sorts.

The addition to the test suite showcases the usage.
---
 test-suite/success/polymorphism.v | 32 +++++++++++++++++++++++++++++++-
 1 file changed, 31 insertions(+), 1 deletion(-)

(limited to 'test-suite/success')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 878875bd92..0a58fe89a1 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -321,4 +321,34 @@ Definition unwrap' := fun (X : Type) (b : box X) => let (unw) := b in unw.
 Fail Definition bad : False := TypeNeqSmallType.paradox (unwrap' Type (wrap _
 Type)) eq_refl.
 
-End Hurkens'.
\ No newline at end of file
+End Hurkens'.
+
+Module Anonymous.
+  Set Universe Polymorphism.
+
+  Definition defaultid := (fun x => x) : Type -> Type.
+  Definition collapseid := defaultid@{_ _}.
+  Check collapseid@{_}.
+
+  Definition anonid := (fun x => x) : Type -> Type@{_}.
+  Check anonid@{_}.
+
+  Definition defaultalg := Type : Type.
+  Definition usedefaultalg := defaultalg@{_ _}.
+  Check usedefaultalg@{_ _}.
+
+  Definition anonalg := (fun x => x) (Type : Type@{_}).
+  Check anonalg@{_}.
+
+  Definition unrelated@{i j} := nat.
+  Definition useunrelated := unrelated@{_ _}.
+  Check useunrelated@{_ _}.
+
+  Definition inthemiddle@{i j k} :=
+    let _ := defaultid@{i j} in
+    defaultalg@{k j}.
+  (* i <= j < k *)
+  Definition collapsethemiddle := inthemiddle@{i _ j}.
+  Check collapsethemiddle@{_ _}.
+
+End Anonymous.
-- 
cgit v1.2.3


From 4361c1ed9ac5646055f9f0eecc4a003d720c1994 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Wed, 12 Apr 2017 13:29:16 +0200
Subject: Type@{_} should not produce a flexible algebraic universe.

Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
---
 test-suite/success/polymorphism.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'test-suite/success')

diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 0a58fe89a1..66ff55edcb 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -333,12 +333,12 @@ Module Anonymous.
   Definition anonid := (fun x => x) : Type -> Type@{_}.
   Check anonid@{_}.
 
-  Definition defaultalg := Type : Type.
-  Definition usedefaultalg := defaultalg@{_ _}.
+  Definition defaultalg := (fun x : Type => x) (Type : Type).
+  Definition usedefaultalg := defaultalg@{_ _ _}.
   Check usedefaultalg@{_ _}.
 
-  Definition anonalg := (fun x => x) (Type : Type@{_}).
-  Check anonalg@{_}.
+  Definition anonalg := (fun x : Type@{_} => x) (Type : Type).
+  Check anonalg@{_ _}.
 
   Definition unrelated@{i j} := nat.
   Definition useunrelated := unrelated@{_ _}.
@@ -346,7 +346,7 @@ Module Anonymous.
 
   Definition inthemiddle@{i j k} :=
     let _ := defaultid@{i j} in
-    defaultalg@{k j}.
+    anonalg@{k j}.
   (* i <= j < k *)
   Definition collapsethemiddle := inthemiddle@{i _ j}.
   Check collapsethemiddle@{_ _}.
-- 
cgit v1.2.3


From cff6f53cbef53ce3902e59853f7a7dc9b7150f45 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 1 May 2017 13:25:10 +0200
Subject: Adding a test-suite pattern-unification example that Econstr fixed.

---
 test-suite/success/unification.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 296686e16e..6f7498d659 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -188,3 +188,14 @@ Proof.
   apply idpath.
   apply idpath.
 Defined.
+
+(* An example where it is necessary to evar-normalize the instance of
+   an evar to evaluate if it is a pattern *)
+
+Check
+  let a := ?[P] in
+  fun (H : forall y (P : nat -> Prop), y = 0 -> P y)
+      x (p:x=0) =>
+    H ?[y] a p : x = 0.
+(* We have to solve "?P ?y[x] == x = 0" knowing from
+   "p : (x=0) == (?y[x] = 0)" that "?y := x" *)
-- 
cgit v1.2.3


From e2de94b90e8802fa5c5dc33c7daf6b8ce5646bfa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 14 May 2017 00:10:57 +0200
Subject: Fixing a bug with nested "as" clauses in "match".

---
 test-suite/success/Cases.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 49c465b6c6..52fe98ac07 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -1868,3 +1868,8 @@ Definition transport {A} (P : A->Type) {x y : A} (p : x=y) (u : P x) : P y :=
 Check match eq_refl 0 in _=O return O=O with eq_refl => eq_refl end.
 
 Check match niln in listn O return O=O with niln => eq_refl end.
+
+(* A test about nested "as" clauses *)
+(* (was failing up to May 2017) *)
+
+Check fun x => match x with (y,z) as t as w => (y+z,t) = (0,w) end.
-- 
cgit v1.2.3


From b82f27726f5ae891689e3b958323c2a61d4c154b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 22:31:08 +0200
Subject: Fixing grammar for "evar" by exporting the test_lpar_id_colon trick
 to EXTEND.

---
 test-suite/success/ltac.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite/success')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index ce90990594..9ab47fedea 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -317,3 +317,9 @@ let T := constr:(fun a b : nat => a) in
   end.
 exact (eq_refl n).
 Qed.
+
+(* Test evar syntax *)
+
+Goal True.
+evar (0=0).
+Abort.
-- 
cgit v1.2.3