20 files changed, 153 insertions, 21 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 285460762b..e15094ccfa 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -27,8 +27,8 @@
 
 # Default value when called from a freshly compiled Coq, but can be
 # easily overridden
-BIN := $(shell cd ..; readlink -f bin)/
 LIB := $(shell cd ..; pwd)
+BIN := $(LIB)/bin/
 
 coqtop := $(BIN)coqtop -coqlib $(LIB) -boot -q -batch -test-mode -R prerequisite TestSuite
 coqc := $(BIN)coqc -coqlib $(LIB) -R prerequisite TestSuite
@@ -45,7 +45,7 @@ REDIR := $(if $(VERBOSE),,> /dev/null 2>&1)
 
 # read out an emacs config and look for coq-prog-args; if such exists, return it
 get_coq_prog_args_helper = sed -n s'/^.*coq-prog-args:[[:space:]]*(\([^)]*\)).*/\1/p' $(1)
-get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1)))) 
+get_coq_prog_args = $(strip $(shell $(call get_coq_prog_args_helper,$(1))))
 SINGLE_QUOTE="
 #" # double up on the quotes, in a comment, to appease the emacs syntax highlighter
 # wrap the arguments in parens, but only if they exist
@@ -68,6 +68,7 @@ ifeq (,$(bogomips))
   $(warning cannot run complexity tests (no bogomips found))
 endif
 
+# keep these synced with test-suite/save-logs.sh
 log_success = "==========> SUCCESS <=========="
 log_segfault = "==========> FAILURE <=========="
 log_anomaly = "==========> FAILURE <=========="
@@ -164,7 +165,13 @@ summary.log:
 	$(SHOW) BUILDING SUMMARY FILE
 	$(HIDE)$(MAKE) --quiet summary > "$@"
 
+# if not on travis we can get the log files (they're just there for a
+# local build, and downloadable on GitLab)
 report: summary.log
+	$(HIDE)./save-logs.sh
+	$(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:start:coq.logs'; fi
+	$(HIDE)if [ -n "${TRAVIS}" ]; then find logs/ -name '*.log' -not -name 'summary.log' -exec cat '{}' ';'; fi
+	$(HIDE)if [ -n "${TRAVIS}" ]; then echo 'travis_fold:end:coq.logs'; fi
 	$(HIDE)if grep -q -F 'Error!' summary.log ; then echo FAILURES; grep -F 'Error!' summary.log; false; else echo NO FAILURES; fi
 
 #######################################################################
diff --git a/test-suite/bugs/closed/5233.v b/test-suite/bugs/closed/5233.v
new file mode 100644
index 0000000000..06286c740d
--- /dev/null
+++ b/test-suite/bugs/closed/5233.v
@@ -0,0 +1,2 @@
+(* Implicit arguments on type were missing for recursive records *)
+Inductive foo {A : Type} : Type := { Foo : foo }.
diff --git a/test-suite/bugs/closed/5523.v b/test-suite/bugs/closed/5523.v
new file mode 100644
index 0000000000..d7582a3797
--- /dev/null
+++ b/test-suite/bugs/closed/5523.v
@@ -0,0 +1,6 @@
+(* Support for complex constructions in recursive notations, especially "match". *)
+
+Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x := let y := x in f y.
+Notation "'dlet' x , y := v 'in' ( a , b , .. , c )"
+  := (Let_In v (fun '(x, y) => pair .. (pair a b) .. c))
+       (at level 0).
diff --git a/test-suite/coq-makefile/native1/run.sh b/test-suite/coq-makefile/native1/run.sh
index bc9f846dda..f079662631 100755
--- a/test-suite/coq-makefile/native1/run.sh
+++ b/test-suite/coq-makefile/native1/run.sh
@@ -3,7 +3,8 @@
 #set -x
 set -e
 
-if which ocamlopt; then
+NATIVECOMP=`grep "let no_native_compiler = false" ../../../config/coq_config.ml`||true
+if [[ `which ocamlopt` && $NATIVECOMP ]]; then
 
 . ../template/init.sh
 	
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 4d59a92cbf..f4ecfd7362 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -98,5 +98,10 @@ fun n : nat => foo4 n (fun _ y : nat => ETA z : nat, (fun _ : nat => y = 0))
      : nat -> Prop
 tele (t : Type) '(y, z) (x : t0) := tt
      : forall t : Type, nat * nat -> t -> fpack
+[fun x : nat => x + 0;; fun x : nat => x + 1;; fun x : nat => x + 2]
+     : (nat -> nat) *
+       ((nat -> nat) *
+        ((nat -> nat) *
+         ((nat -> nat) * ((nat -> nat) * ((nat -> nat) * (nat -> nat))))))
 foo5 x nat x
      : nat -> nat
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 96d831944f..71536c68fb 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -140,6 +140,12 @@ Notation "'tele' x .. z := b" :=
 
 Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt.
 
+(* Checking that "fun" in a notation does not mixed up with the
+   detection of a recursive binder *)
+
+Notation "[ x ;; .. ;; y ]" := ((x,((fun u => S u), .. (y,(fun u => S u,fun v:nat => v)) ..))).
+Check [ fun x => x+0 ;; fun x => x+1 ;; fun x => x+2 ].
+
 (* Cyprien's part of bug #4765 *)
 
 Notation foo5 x T y := (fun x : T => y).
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index bf1bf2809d..ca56f032ff 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -1,12 +1,10 @@
-3 subgoals (ID 29)
+3 subgoals (ID 31)
   
   H : 0 = 0
   ============================
   1 = 1
 
-subgoal 2 (ID 33) is:
+subgoal 2 (ID 35) is:
  1 = S (S m')
-subgoal 3 (ID 20) is:
+subgoal 3 (ID 22) is:
  S (S n') = S m
-
-(dependent evars: (printing disabled) )
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index c70467912f..d28ee42761 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x : T n := A n in ?t ?y : T n
+fun n : nat => let y : T n := A n in ?t ?x : T n
      : forall n : nat, T n
 where
-?t : [n : nat  x := A n : T n |- ?T -> T n] 
-?y : [n : nat  x := A n : T n |- ?T] 
-fun n : nat => ?t ?y : T n
+?t : [n : nat  y := A n : T n |- ?T -> T n] 
+?x : [n : nat  y := A n : T n |- ?T] 
+fun n : nat => ?t ?x : T n
      : forall n : nat, T n
 where
 ?t : [n : nat |- ?T -> T n] 
-?y : [n : nat |- ?T] 
+?x : [n : nat |- ?T] 
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 1825db1676..f761a4dc5a 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -27,5 +27,5 @@ Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 (* Note: exact numbers of evars are not important... *)
 
 Inductive T (n:nat) : Type := A : T n.
-Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n (y:=A n:T n) => _ _ : T n.
 Check fun n => _ _ : T n.
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 9471b892dd..48be63a46a 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -3,3 +3,9 @@ In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
 while it is expected to have type "{x : nat | x = y}".
+1 focused subgoal
+(shelved: 1)
+  
+  H : ?n <= 3 -> 3 <= ?n -> ?n = 3
+  ============================
+  True
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
index b3b5071a03..f1efd0df2a 100644
--- a/test-suite/output/names.v
+++ b/test-suite/output/names.v
@@ -3,3 +3,7 @@
 
 Parameter a : forall x, {y:nat|x=y}.
 Fail Definition b y : {x:nat|x=y} := a y.
+
+Goal (forall n m, n <= m -> m <= n -> n = m) -> True.
+intro H; epose proof (H _ 3) as H.
+Show.
diff --git a/test-suite/save-logs.sh b/test-suite/save-logs.sh
new file mode 100755
index 0000000000..fb8a1c1b0a
--- /dev/null
+++ b/test-suite/save-logs.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+
+SAVEDIR="logs"
+
+# reset for local builds
+rm -rf "$SAVEDIR"
+mkdir "$SAVEDIR"
+
+# keep this synced with test-suite/Makefile
+FAILMARK="==========> FAILURE <=========="
+
+FAILED=$(mktemp)
+find . '(' -path ./bugs/opened -prune ')' -o '(' -name '*.log' -exec grep "$FAILMARK" -q '{}' ';' -print0 ')' > "$FAILED"
+
+rsync -a --from0 --files-from="$FAILED" . "$SAVEDIR"
+cp summary.log "$SAVEDIR"/
+
+# cleanup
+rm "$FAILED"
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index ffd50f6efd..69dc9aca78 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,4 +1,3 @@
-
 (* Cf coqbugs #546 *)
 
 Require Import Omega.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index f07773f8bd..921433cadd 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -27,3 +27,8 @@ Parameters (a:_) (b:a=0).
 Definition foo6 (x:=1) : forall {n:nat}, n=n := fun n => eq_refl.
 
 Fixpoint foo7 (x:=1) (n:nat) {p:nat} {struct n} : nat.
+
+(* Some example which should succeed with local implicit arguments *)
+
+Inductive A {P:forall m {n}, n=m -> Prop} := C : P 0 eq_refl -> A.
+Inductive B (P:forall m {n}, n=m -> Prop) := D : P 0 eq_refl -> B P.
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 8334322c99..6f27c1d369 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -87,3 +87,8 @@ Record R : Type := {
   P (A : Type) : Prop := exists x : A -> A, x = x;
   Q A : P A -> P A
 }.
+
+(* We allow reusing an implicit parameter named in non-recursive types *)
+(* This is used in a couple of development such as UniMatch *)
+
+Record S {A:Type} := { a : A; b : forall A:Type, A }.
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index 43e3493c1e..ca37467166 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -20,3 +20,9 @@ Inductive U := A.
 Bind Scope u with U.
 Notation "'ε'" := A : u.
 Definition c := ε : U.
+
+(* Check activation of type scope for tactics such as assert *)
+
+Goal True.
+assert (nat * nat).
+
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
index 5b9265b6a8..05ab913932 100644
--- a/test-suite/success/coindprim.v
+++ b/test-suite/success/coindprim.v
@@ -13,9 +13,10 @@ Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}.
 CoFixpoint ones := {| hd := 1; tl := ones |}.
 CoFixpoint ticks := {| hd := tt; tl := ticks |}.
 
-CoInductive stream_equiv {A} {s : Stream A} {s' : Stream A} : Prop :=
-  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv _ s.(tl) s'.(tl) }.
-Arguments stream_equiv {A} s s'.
+CoInductive stream_equiv {A} (s : Stream A) (s' : Stream A) : Prop :=
+  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv s.(tl) s'.(tl) }.
+Arguments hdeq {A} {s} {s'}.
+Arguments tleq {A} {s} {s'}.
 
 Program CoFixpoint ones_eq : stream_equiv ones ones.(tl) :=
   {| hdeq := eq_refl; tleq := ones_eq |}.
@@ -88,4 +89,4 @@ Lemma eq (x : U) : x = force x.
 Proof.
   Fail destruct x.
 Abort.
-  (* Impossible *)
-\ No newline at end of file
+  (* Impossible *)
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 4e2bf45118..82f726fa7c 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -62,7 +62,7 @@ Check
 
 Check (fun f:(forall (v:Type->Type), v (v nat) -> nat) => f _ (Some (Some O))).
 
-(* This used to fail with anomaly (Pp.str "evar was not declared") in V8.0pl3 *)
+(* This used to fail with anomaly (Pp.str "evar was not declared.") in V8.0pl3 *)
 
 Theorem contradiction : forall p, ~ p -> p -> False.
 Proof. trivial. Qed.
diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
new file mode 100644
index 0000000000..0ed5b524f3
--- /dev/null
+++ b/test-suite/success/forward.v
@@ -0,0 +1,18 @@
+(* Testing forward reasoning *)
+
+Goal 0=0.
+Fail assert (_ = _).
+eassert (_ = _)by reflexivity.
+eassumption.
+Qed.
+
+Goal 0=0.
+Fail set (S ?[nl]).
+eset (S ?[n]).
+remember (S ?n) as x.
+instantiate (n:=0).
+Fail remember (S (S _)).
+eremember (S (S ?[x])).
+instantiate (x:=0).
+reflexivity.
+Qed.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 4b41a509e5..f12db8b081 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -17,6 +17,29 @@ specialize (eq_trans (x:=a)(y:=b)). intros _.
 specialize (eq_trans H H0). intros _.
 specialize (eq_trans H0 (z:=b)). intros _.
 
+(* incomplete bindings: y is left quantified and z is instantiated. *)
+specialize eq_trans with (x:=a)(z:=c).
+intro h.
+(* y can be instantiated now *)
+specialize h with (y:=b).
+(* z was instantiated above so this must fail. *)
+Fail specialize h with (z:=c).
+clear h.
+
+(* incomplete bindings: 1st dep hyp is instantiated thus A, x and y
+   instantiated too. *)
+specialize eq_trans with (1:=H).
+intro h.
+(* 2nd dep hyp can be instantiated now, which instatiates z too. *)
+specialize h with (1:=H0).
+(* checking that there is no more products in h. *)
+match type of h with
+| _ = _ => idtac
+| _ => fail "specialize test failed: hypothesis h should be an equality at this point"
+end.
+clear h.
+
+
 (* local "in place" specialization *)
 assert (Eq:=eq_trans).
 
@@ -31,6 +54,27 @@ specialize (Eq _ a b c). Undo.
 specialize (Eq _ _ _ _ H H0). Undo.
 specialize (Eq _ _ _ b H0). Undo.
 
+(* incomplete binding *)
+specialize Eq with (y:=b).
+(* A and y have been instantiated so this works *)
+specialize (Eq _ _ H H0).
+Undo 2.
+
+(* incomplete binding (dependent) *)
+specialize Eq with (1:=H).
+(* A, x and y have been instantiated so this works *)
+specialize (Eq _ H0).
+Undo 2.
+
+(* incomplete binding (dependent) *)
+specialize Eq with (1:=H) (2:=H0).
+(* A, x and y have been instantiated so this works *)
+match type of Eq with
+| _ = _ => idtac
+| _ => fail "specialize test failed: hypothesis Eq should be an equality at this point"
+end.
+Undo 2.
+
 (*
 (** strange behavior to inspect more precisely *)
 
@@ -40,7 +84,7 @@ specialize (Eq _ _ _ b H0). Undo.
 (* 2) echoue moins lorsque zero premise de mangé *)
 specialize eq_trans with (1:=Eq).  (* mal typé !! *)
 
-(* 3) *)
+(* 3) Seems fixed.*)
 specialize eq_trans with _ a b c. intros _.
 (* Anomaly: Evar ?88 was not declared. Please report. *)
 *)