6 files changed, 73 insertions, 4 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index ba85286dd3..b99d80e95f 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/Makefile b/test-suite/Makefile
index a26f66285f..e15094ccfa 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -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/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/Show.out b/test-suite/output/Show.out
index 8acfed5d00..ca56f032ff 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -8,5 +8,3 @@ subgoal 2 (ID 35) is:
  1 = S (S m')
 subgoal 3 (ID 22) is:
  S (S n') = S m
-
-(dependent evars: (printing disabled) )
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/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. *)
 *)