5 files changed, 106 insertions, 6 deletions
diff --git a/test-suite/dune b/test-suite/dune
index 6ab2988331..1864153021 100644
--- a/test-suite/dune
+++ b/test-suite/dune
@@ -9,6 +9,10 @@
  (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted ../../install/%{context_name}/lib/coq/ ))))
 
 (rule
+ (targets bin.inc)
+ (action (with-stdout-to %{targets} (run ./ocaml_pwd.exe -quoted -trailing-slash ../../install/%{context_name}/bin/ ))))
+
+(rule
  (targets summary.log)
  (deps
    ; File that should be promoted.
@@ -44,4 +48,4 @@
    ; %{bin:fake_ide}
  (action
   (progn
-   (bash "make -j %{env:NJOBS=2} BIN= COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
+   (bash "make -j %{env:NJOBS=2} BIN=%{read:bin.inc} COQLIB=%{read:libpath.inc} PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests}"))))
diff --git a/test-suite/misc/coq_environment.sh b/test-suite/misc/coq_environment.sh
new file mode 100755
index 0000000000..667d11f89e
--- /dev/null
+++ b/test-suite/misc/coq_environment.sh
@@ -0,0 +1,51 @@
+#!/usr/bin/env bash
+
+export COQBIN=$BIN
+export PATH=$COQBIN:$PATH
+
+TMP=`mktemp -d`
+cd $TMP
+
+cat > coq_environment.txt <<EOT
+# we override COQLIB because we can
+COQLIB="$TMP/overridden" # bla bla
+OCAMLFIND="$TMP/overridden"
+FOOBAR="one more"
+EOT
+
+cp $BIN/coqc .
+cp $BIN/coq_makefile .
+mkdir -p overridden/tools/
+cp $COQLIB/tools/CoqMakefile.in overridden/tools/
+
+unset COQLIB
+N=`./coqc -config | grep COQLIB | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQLIB not overridden by coq_environment
+  coqc -config
+  exit 1
+fi
+N=`./coqc -config | grep OCAMLFIND | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo OCAMLFIND not overridden by coq_environment
+  coqc -config
+  exit 1
+fi
+./coq_makefile -o CoqMakefile -R . foo > /dev/null
+N=`grep COQMF_OCAMLFIND CoqMakefile.conf | grep /overridden | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQMF_OCAMLFIND not overridden by coq_environment
+  cat CoqMakefile.conf
+  exit 1
+fi
+
+export COQLIB="/overridden2"
+N=`./coqc -config | grep COQLIB | grep /overridden2 | wc -l`
+if [ $N -ne 1 ]; then
+  echo COQLIB not overridden by COQLIB when coq_environment present
+  coqc -config
+  exit 1
+fi
+
+rm -rf $TMP
+exit 0
diff --git a/test-suite/ocaml_pwd.ml b/test-suite/ocaml_pwd.ml
index afa3deea3a..054a921b93 100644
--- a/test-suite/ocaml_pwd.ml
+++ b/test-suite/ocaml_pwd.ml
@@ -1,7 +1,26 @@
+open Arg
+
+let quoted = ref false
+let trailing_slash = ref false
+
+let arguments = [
+  "-quoted",Set quoted, "Quote path";
+  "-trailing-slash",Set trailing_slash, "End the path with a /";
+]
+let subject = ref None
+let set_subject x =
+  if !subject <> None then
+    failwith "only one path";
+  subject := Some x
+
 let _ =
-  let quoted = Sys.argv.(1) = "-quoted" in
-  let ch_dir = Sys.argv.(if quoted then 2 else 1) in
-  Sys.chdir ch_dir;
+  Arg.parse arguments set_subject "Usage:";
+  let subject =
+    match !subject with
+    | None -> failwith "no path given";
+    | Some x -> x in
+  Sys.chdir subject;
   let dir = Sys.getcwd () in
-  let dir = if quoted then Filename.quote dir else dir in
+  let dir = if !trailing_slash then dir ^ "/" else dir in
+  let dir = if !quoted then Filename.quote dir else dir in
   Format.printf "%s%!" dir
diff --git a/test-suite/success/change_case.v b/test-suite/success/change_case.v
new file mode 100644
index 0000000000..490e4f4b6c
--- /dev/null
+++ b/test-suite/success/change_case.v
@@ -0,0 +1,20 @@
+Inductive box (A : Type) := Box : A -> box A.
+
+Axiom PRED : unit -> Prop.
+Axiom FUN : forall (u : unit), box (PRED u).
+
+Axiom U : unit.
+Definition V := U.
+
+Goal match FUN U with Box _ _ => True end.
+Proof.
+repeat match goal with
+| [ |- context G[ U ] ] =>
+ let e := context G [ V ] in
+ change e
+end.
+set (Z := V).
+clearbody Z. (* This fails if change misses the case parameters *)
+destruct (FUN Z).
+constructor.
+Qed.
diff --git a/test-suite/success/rewrite_in.v b/test-suite/success/rewrite_in.v
index 29fe915ff4..3433866239 100644
--- a/test-suite/success/rewrite_in.v
+++ b/test-suite/success/rewrite_in.v
@@ -5,4 +5,10 @@ Goal forall (P Q : Prop) (f:P->Prop) (p:P), (P<->Q) -> f p -> True.
   rewrite H in p || trivial.
 Qed.
 
-
+Goal 1 = 0 -> 0 = 1.
+  intro H.
+  Fail rewrite H at 1 2 3. (* bug #13566 *)
+  Fail rewrite H at 0.
+  rewrite H at 1.
+  reflexivity.
+Qed.