From 21e1d501e17c9989d9cd689988a510e1864f817a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Oct 2016 15:43:39 +0200
Subject: Attempt to improve error rendering in pattern-matching compilation
 (#5142).

When trying different possible return predicates, returns the error
given by the first try, assuming this is the most interesting one.
---
 test-suite/output/Cases.out |  3 +++
 test-suite/output/Cases.v   | 12 ++++++++++++
 2 files changed, 15 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 2b828d382a..95fcd362ef 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -56,3 +56,6 @@ match H with
      else fun _ : P false => Logic.I) x
 end
      : B -> True
+The command has indeed failed with message:
+Non exhaustive pattern-matching: no clause found for pattern 
+gadtTy _ _
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 3c2eaf42c9..1903753cc5 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -77,3 +77,15 @@ destruct b as [|] ; exact Logic.I.
 Defined.
 
 Print f.
+
+(* Was enhancement request #5142 (error message reported on the most
+   general return clause heuristic) *)
+
+Inductive gadt : Type -> Type :=
+| gadtNat : nat -> gadt nat
+| gadtTy : forall T, T -> gadt T.
+
+Fail Definition gadt_id T (x: gadt T) : gadt T :=
+  match x with
+  | gadtNat n => gadtNat n
+  end.
-- 
cgit v1.2.3


From 00978cddf6e2da71892de6362e69c372429e159f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Oct 2016 17:20:06 +0200
Subject: Test for variant of #5142 (good error message on pattern-matching
 failure).

---
 test-suite/output/Cases.out | 13 +++++++++++++
 test-suite/output/Cases.v   | 17 +++++++++++++++++
 2 files changed, 30 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 95fcd362ef..8ce6f9795c 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -59,3 +59,16 @@ end
 The command has indeed failed with message:
 Non exhaustive pattern-matching: no clause found for pattern 
 gadtTy _ _
+The command has indeed failed with message:
+In environment
+texpDenote : forall t : type, texp t -> typeDenote t
+t : type
+e : texp t
+t1 : type
+t2 : type
+t0 : type
+b : tbinop t1 t2 t0
+e1 : texp t1
+e2 : texp t2
+The term "0" has type "nat" while it is expected to have type
+ "typeDenote t0".
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 1903753cc5..4074896420 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -89,3 +89,20 @@ Fail Definition gadt_id T (x: gadt T) : gadt T :=
   match x with
   | gadtNat n => gadtNat n
   end.
+
+(* A variant of #5142 (see Satrajit Roy's example on coq-club (Oct 17, 2016)) *)
+
+Inductive type:Set:=Nat.
+Inductive tbinop:type->type->type->Set:= TPlus : tbinop Nat Nat Nat.
+Inductive texp:type->Set:=
+ |TNConst:nat->texp Nat
+ |TBinop:forall t1 t2 t, tbinop t1 t2 t->texp t1->texp t2->texp t.
+Definition typeDenote(t:type):Set:= match t with Nat => nat end.
+
+(* We expect a failure on TBinop *)
+Fail Fixpoint texpDenote t (e:texp t):typeDenote t:=
+  match e with
+  | TNConst n => n
+  | TBinop t1 t2 _ b e1 e2 => O
+  end.
+
-- 
cgit v1.2.3


From 2dfe032fd42f2489320936fe1e60c9cf7dafe8cf Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 3 Mar 2016 18:26:12 +0100
Subject: [search] Don't build intermediate lists in search.

This patch converts the `search_*` functions to use an iter-style API.

Consequently, the Search Vernac will produce a message for each search
result, greatly improving roundtrip time as IDEs can effectively display
the results in a streaming way.

It also allows different printers to be used.

I didn't observe a performance difference (as things seem to be
dominated by printing and `Declaremods`).

As a minor tweak, we make search with "Output Name Only" more efficient.

Motivation:
-----------

Currently, the main search API `Search.generic_search` is an effectful,
iteration-based function:

```ocaml
val generic_search : int option -> display_function -> unit
```

This type is imposed by `Declaremods`, which exposes an effectful,
iteration-based API to traverse Coq library objects.

The `Search.search_*` functions try to offer a more functional API by
returning a list of pretty printing commands. They need to build an
internal intermediate list for that purpose.

However, this is a waste of time, as the destination of these lists is
to be flushed out by the printer right away.
---
 test-suite/output/SearchPattern.out | 2 --
 1 file changed, 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index 1eb7eca8f1..f3c12effca 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -40,7 +40,6 @@ Nat.land: nat -> nat -> nat
 Nat.lor: nat -> nat -> nat
 Nat.ldiff: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-
 S: nat -> nat
 Nat.succ: nat -> nat
 Nat.pred: nat -> nat
@@ -74,7 +73,6 @@ le_n: forall n : nat, n <= n
 pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-
 h: n <> newdef n
 h: n <> newdef n
 h: P n
-- 
cgit v1.2.3


From ecaea9a428c052ea431ec7c392e81aaf918d5d96 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 10 Oct 2016 17:28:05 +0200
Subject: Fix minimization to be insensitive to redundant arcs.

The new algorithm produces different sets of arcs than in 8.5, hence
existing developments may fail to pass now because they relied on
the (correct but more approximate) result of minimization in 8.5 which
wasn't insensitive.

The algorithm works bottom-up on the (well-founded) graph to
find lower levels that an upper level can be minimized to. We
filter said lower levels according to the lower sets of the other levels
we consider. If they appear in any of them then we don't need their
constraints. Does not seem to have a huge impact on performance in HoTT,
but this should be evaluated further.

Adapt test-suite files accordingly.
---
 test-suite/bugs/closed/4527.v | 6 +++---
 test-suite/bugs/closed/4544.v | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 4ca6fe78cd..08628377f0 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -249,10 +249,10 @@ Section Reflective_Subuniverse.
  exact H.
     Defined.
 
-    Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : 
+    Definition inO_paths@{i} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : 
 S)    : In@{Ou Oa i} O (x=y).
     Proof.
-      simple refine (inO_to_O_retract@{i j} _ _ _); intro u.
+      simple refine (inO_to_O_retract@{i} _ _ _); intro u.
       -
  assert (p : (fun _ : O (x=y) => x) == (fun _=> y)).
         {
@@ -264,4 +264,4 @@ S)    : In@{Ou Oa i} O (x=y).
  hnf.
         rewrite O_indpaths_beta; reflexivity.
     Qed.
-    Check inO_paths@{Type Type}.
+    Check inO_paths@{Type}.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index 048f31ce3d..da140c9318 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -652,7 +652,7 @@ Defined.
 
   Definition ReflectiveSubuniverse := Modality.
 
-  Definition O_reflector := O_reflector.
+  Definition O_reflector@{u a i} := O_reflector@{u a i}.
 
   Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
                    Type2le@{i a} -> Type2le@{i a}
@@ -660,7 +660,7 @@ Defined.
   Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
                                In@{u a i} O (O_reflector@{u a i} O T)
     := O_inO@{u a i}.
-  Definition to := to.
+  Definition to@{u a i} := to@{u a i}.
   Definition inO_equiv_inO@{u a i j k} :
       forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j})
              (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f),
-- 
cgit v1.2.3


From a07f67f6f1deba8b14672c618c003ec345d7970a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Sep 2016 16:37:04 +0200
Subject: A fix for #5097 (status of evars refined by "clear" in ltac: closed
 wrt evars).

If an existing evar was cleared in pretyping (typically while
processing "ltac:"), it created an evar considered as new. Updating
them instead along the "cleared" flag.

If correct, I suspect similar treatment should be done for refining
along "change", "rename" and "move".
---
 test-suite/bugs/closed/5097.v | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 test-suite/bugs/closed/5097.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v
new file mode 100644
index 0000000000..37b239cf61
--- /dev/null
+++ b/test-suite/bugs/closed/5097.v
@@ -0,0 +1,7 @@
+(* Tracing existing evars along the weakening rule ("clear") *)
+Goal forall y, exists x, x=0->x=y.
+intros.
+eexists ?[x].
+intros.
+let x:=constr:(ltac:(clear y; exact 0)) in idtac x.
+Abort.
-- 
cgit v1.2.3


From 6d5fe92efbe3f6269666644a0f2e8e9aab8ab307 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 19 Oct 2016 10:08:49 +0200
Subject: Adding dependency of the test-suite subsystems in prerequisite
 (fixing #5150).

---
 test-suite/Makefile | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index f1cb21ecd5..8500ef1b3d 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -221,7 +221,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
@@ -253,7 +253,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -267,7 +267,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
+$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -289,7 +289,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out
 	  rm $$tmpoutput; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -307,7 +307,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v
 # the .v file with exactly two digits after the dot. The reference for
 # time is a 6120 bogomips cpu.
 ifneq (,$(bogomips))
-$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -338,7 +338,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v
 endif
 
 # Ideal-features tests
-$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v
+$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-- 
cgit v1.2.3


From 5b0b6c92354c34a4f0d5551f88b16264fb08be5f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 21 Oct 2016 10:49:15 +0200
Subject: Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3

This makes [refine] typecheck the term only once (instead of twice),
(Qed excluded of course). Fix test-suite file for output of constraints
accordingly.
---
 test-suite/output/unifconstraints.out | 26 ++++----------------------
 1 file changed, 4 insertions(+), 22 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out
index d152052ba3..ae84603622 100644
--- a/test-suite/output/unifconstraints.out
+++ b/test-suite/output/unifconstraints.out
@@ -8,11 +8,7 @@ subgoal 2 is:
  forall n : nat, ?Goal n -> ?Goal (S n)
 subgoal 3 is:
  nat
-unification constraints:
- ?Goal ?Goal2 <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  ?Goal ?Goal2 <=
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
@@ -28,11 +24,7 @@ subgoal 2 is:
  forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0)
 subgoal 3 is:
  nat
-unification constraints:
- ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <=
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
@@ -48,12 +40,7 @@ subgoal 2 is:
  forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0)
 subgoal 3 is:
  nat
-unification constraints:
- 
- n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  
  n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <=
    True /\ True /\ True \/
@@ -70,12 +57,7 @@ subgoal 2 is:
  forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0)
 subgoal 3 is:
  nat
-unification constraints:
- 
- n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <=
-   True /\ True /\ True \/
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier =
-   veeryyyyyyyyyyyyloooooooooooooonggidentifier
+unification constraint:
  
  n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <=
    True /\ True /\ True \/
-- 
cgit v1.2.3


From 5609da1e08f950fab85b87b257ed343b491f1ef5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 21 Oct 2016 17:57:18 +0200
Subject: Revert "unification.ml: fix for bug #4763, unif regression"

This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a.

A good fix requires to review a bit the design of unification constraint
postponement, which we do in 8.6. We leave things as they are in 8.5 for
compatibility.
---
 test-suite/bugs/closed/4763.v | 13 -------------
 1 file changed, 13 deletions(-)
 delete mode 100644 test-suite/bugs/closed/4763.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
deleted file mode 100644
index ae8ed0e6e8..0000000000
--- a/test-suite/bugs/closed/4763.v
+++ /dev/null
@@ -1,13 +0,0 @@
-Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses.
-Coercion is_true : bool >-> Sortclass.
-Global Instance: Transitive leb.
-Admitted.
-
-Goal forall x y z, leb x y -> leb y z -> True.
-  intros ??? H H'.
-  lazymatch goal with
-  | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ]
-    => pose proof (transitivity H H' : is_true (R x z))
-  end.
-  exact I.
-Qed.
\ No newline at end of file
-- 
cgit v1.2.3


From c28a2a3a1297098ee73ad5b26e714164b6167d2b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 21 Oct 2016 18:39:05 +0200
Subject: Adding a test for bug #3495.

---
 test-suite/bugs/closed/3495.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/bugs/closed/3495.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/3495.v b/test-suite/bugs/closed/3495.v
new file mode 100644
index 0000000000..102a2aba0d
--- /dev/null
+++ b/test-suite/bugs/closed/3495.v
@@ -0,0 +1,18 @@
+Require Import RelationClasses.
+
+Axiom R : Prop -> Prop -> Prop.
+Declare Instance : Reflexive R.
+
+Class bar := { x : False }.
+Record foo := { a : Prop ; b : bar }.
+
+Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}.
+
+Goal exists k, R k True.
+Proof.
+eexists.
+evar (b : bar).
+let e := match goal with |- R ?e _ => constr:(e) end in
+unify e (a (default_foo True)).
+subst b.
+reflexivity.
-- 
cgit v1.2.3


From 56744aadd413dd9417d245951083117b05170e14 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Oct 2016 11:38:51 +0200
Subject: Fixing printing of generic arguments of tag "var".

---
 test-suite/output/ltac.out | 1 +
 test-suite/output/ltac.v   | 5 +++++
 2 files changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index d003c70df9..266e4c7243 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,2 +1,3 @@
 The command has indeed failed with message:
 Error: Ltac variable y depends on pattern variable name z which is not bound in current context.
+Hx
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 7e2610c7d7..e5bcff8ddb 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -15,3 +15,8 @@ lazymatch goal with
 | H1 : HT |- _ => idtac
 end.
 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.
-- 
cgit v1.2.3


From 1d769e02b3baba54246c942fe116abaf850892db Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 11:44:24 +0200
Subject: Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit
 too strong.

New fix. A bit less consistent with the spirit of this Makefile as we
list prerequisite files explicitly, but avoid to redo subsystems at
each call to "make" as with previous fix.

Other solutions from experts are welcome.
---
 test-suite/Makefile | 15 +++++++++------
 1 file changed, 9 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 8500ef1b3d..491b16960e 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -84,6 +84,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
 
+PREREQUISITELOG = prerequisite/admit.v.log			\
+  prerequisite/make_local.v.log prerequisite/make_notation.v.log
+
 #######################################################################
 # Phony targets
 #######################################################################
@@ -221,7 +224,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
@@ -253,7 +256,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -267,7 +270,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
+$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -289,7 +292,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
 	  rm $$tmpoutput; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -307,7 +310,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
 # the .v file with exactly two digits after the dot. The reference for
 # time is a 6120 bogomips cpu.
 ifneq (,$(bogomips))
-$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -338,7 +341,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
 endif
 
 # Ideal-features tests
-$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
-- 
cgit v1.2.3


From 5f1dd4c401110d6b10350c847805c6923fa09de5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 17:04:41 +0200
Subject: Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{"
 or "}").

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

(limited to 'test-suite')

diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 2f7c62972a..511b60b4bb 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -110,3 +110,9 @@ Goal True -> True. intros H. exact H. Qed.
 
 (* Check absence of collision on ".." in nested notations with ".." *)
 Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
+
+(* Check parsing of { and } is not affected by notations #3479 *)
+Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
+Goal True.
+{{ exact I. }}
+Qed.
-- 
cgit v1.2.3


From 166634c57bbad2e727364a97bf30bc3d67d2f2a8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 17:36:32 +0200
Subject: Merge branch 'v8.5' into v8.6

+ a few improvements on 5f1dd4c40 (lexing of { and }).
---
 test-suite/Makefile            | 15 +++++++++------
 test-suite/success/Notations.v |  7 +++++++
 2 files changed, 16 insertions(+), 6 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 10eb2df390..6a18c45dfa 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -88,6 +88,9 @@ VSUBSYSTEMS := prerequisite success failure $(BUGS) output \
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk
 
+PREREQUISITELOG = prerequisite/admit.v.log			\
+  prerequisite/make_local.v.log prerequisite/make_notation.v.log
+
 #######################################################################
 # Phony targets
 #######################################################################
@@ -226,7 +229,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard success/*.v micromega/*.v modules/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods -impredicative-set)"; \
@@ -257,7 +260,7 @@ $(addsuffix .log,$(wildcard stm/*.v)): %.v.log: %.v
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -271,7 +274,7 @@ $(addsuffix .log,$(wildcard failure/*.v)): %.v.log: %.v prerequisite
 	  fi; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out prerequisite
+$(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -330,7 +333,7 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
 	  rm $$tmpexpected; \
 	} > "$@"
 
-$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -348,7 +351,7 @@ $(addsuffix .log,$(wildcard interactive/*.v)): %.v.log: %.v prerequisite
 # the .v file with exactly two digits after the dot. The reference for
 # time is a 6120 bogomips cpu.
 ifneq (,$(bogomips))
-$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
@@ -379,7 +382,7 @@ $(addsuffix .log,$(wildcard complexity/*.v)): %.v.log: %.v prerequisite
 endif
 
 # Ideal-features tests
-$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v prerequisite
+$(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  echo $(call log_intro,$<); \
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 30abd961b1..666c912578 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -115,3 +115,10 @@ Notation "[ a , .. , b ]" := (a, (.. (b,tt) ..)).
 Require Import Coq.Vectors.VectorDef.
 Import VectorNotations.
 Goal True. idtac; []. (* important for test: no space here *) constructor. Qed.
+
+(* Check parsing of { and } is not affected by notations #3479 *)
+Notation " |- {{ a }} b" := (a=b) (no associativity, at level 10).
+Goal True.
+{{ exact I. }}
+Qed.
+Check |- {{ 0 }} 0.
-- 
cgit v1.2.3


From 7f69f6d94b751464aae3c852f0bc53d5854f30a4 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 24 Oct 2016 18:36:26 +0200
Subject: Rename lia.cache into .lia.cache in the test-suite Makefile.

---
 test-suite/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 6a18c45dfa..c10cd4ed44 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -105,7 +105,7 @@ run: $(SUBSYSTEMS)
 bugs: $(BUGS)
 
 clean:
-	rm -f trace lia.cache
+	rm -f trace .lia.cache
 	$(SHOW) "RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log>"
 	$(HIDE)find . \( \
 	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' \
-- 
cgit v1.2.3


From 810077167cd6f5077abe7b79b12ae9b51eae1b62 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 24 Oct 2016 22:44:34 +0200
Subject: Adding a test for #4398 (interpretation scopes for "match goal").

---
 test-suite/output/ltac.out | 4 ++++
 test-suite/output/ltac.v   | 9 +++++++++
 2 files changed, 13 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index a62f4312ed..a7bde5ea3f 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -27,3 +27,7 @@ In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
 Error: No primitive equality found.
 Hx
+nat
+nat
+0
+0
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index fb1dab7994..76c37625aa 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -48,3 +48,12 @@ Fail h H.
 Ltac m H := idtac H; exact H.
 Goal True.
 let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
+
+(* Check consistency of interpretation scopes (#4398) *)
+
+Goal nat*(0*0=0) -> nat*(0*0=0). intro.
+match goal with H: ?x*?y |- _ => idtac x end.
+match goal with |- ?x*?y => idtac x end.
+match goal with H: context [?x*?y] |- _ => idtac x end.
+match goal with |- context [?x*?y] => idtac x end.
+Abort.
-- 
cgit v1.2.3