6 files changed, 238 insertions, 12 deletions
diff --git a/test-suite/bugs/closed/bug_4787.v b/test-suite/bugs/closed/bug_4787.v
deleted file mode 100644
index a1444a4f63..0000000000
--- a/test-suite/bugs/closed/bug_4787.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* [Unset Bracketing Last Introduction Pattern] was not working *)
-
-Unset Bracketing Last Introduction Pattern.
-
-Goal forall T (x y : T * T), fst x = fst y /\ snd x = snd y -> x = y.
-do 10 ((intros [] || intro); simpl); reflexivity.
-Qed.
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/output/StringSyntaxPrimitive.out b/test-suite/output/StringSyntaxPrimitive.out
new file mode 100644
index 0000000000..131975c760
--- /dev/null
+++ b/test-suite/output/StringSyntaxPrimitive.out
@@ -0,0 +1,20 @@
+"abc"
+     : intList
+"abc"
+     : intList
+mk_intList [97%int63; 98%int63; 99%int63]
+     : intList
+"abc"
+     : intArray
+"abc"
+     : intArray
+     = "abc"
+     : nestArray
+"abc"
+     : nestArray
+"100"
+     : floatList
+"100"
+     : floatList
+mk_floatList [1%float; 0%float; 0%float]
+     : floatList
diff --git a/test-suite/output/StringSyntaxPrimitive.v b/test-suite/output/StringSyntaxPrimitive.v
new file mode 100644
index 0000000000..23ef082013
--- /dev/null
+++ b/test-suite/output/StringSyntaxPrimitive.v
@@ -0,0 +1,139 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii.
+Require Coq.Array.PArray Coq.Floats.PrimFloat.
+Require Import Coq.Numbers.BinNums Coq.Numbers.Cyclic.Int63.Int63.
+
+Set Printing Depth 100000.
+Set Printing Width 1000.
+
+Close Scope char_scope.
+Close Scope string_scope.
+
+(* Notations for primitive integers inside polymorphic datatypes *)
+Module Test1.
+  Inductive intList := mk_intList (_ : list int).
+  Definition i63_from_byte (b : byte) : int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)).
+  Definition i63_to_byte (i : int) : byte :=
+      match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end.
+
+  Definition to_byte_list '(mk_intList a) := List.map i63_to_byte a.
+
+  Definition from_byte_list (xs : list byte) : intList:=
+    mk_intList (List.map i63_from_byte xs).
+
+  Declare Scope intList_scope.
+  Delimit Scope intList_scope with intList.
+
+  String Notation intList from_byte_list to_byte_list : intList_scope.
+
+  Open Scope intList_scope.
+  Import List.ListNotations.
+  Check mk_intList [97; 98; 99]%int63%list.
+  Check "abc"%intList.
+
+  Definition int' := int.
+  Check mk_intList (@cons int' 97 [98; 99])%int63%list.
+End Test1.
+
+Import PArray.
+
+(* Notations for primitive arrays *)
+Module Test2.
+  Inductive intArray := mk_intArray (_ : array int).
+
+  Definition i63_from_byte (b : byte) : Int63.int := Int63.of_Z (BinInt.Z.of_N (Byte.to_N b)).
+  Definition i63_to_byte (i : Int63.int) : byte :=
+  match Byte.of_N (BinInt.Z.to_N (Int63.to_Z i)) with Some x => x | None => x00%byte end.
+
+  Definition i63_to_nat x := BinInt.Z.to_nat (Int63.to_Z x).
+  Local Definition nat_length {X} (x : array X) :nat := i63_to_nat (length x).
+
+  Local Fixpoint list_length_i63 {A} (xs : list A) :int :=
+            match xs with
+            | nil => 0
+            | cons _ xs => 1 + list_length_i63 xs
+            end.
+
+  Definition to_byte_list '(mk_intArray a) :=
+    ((fix go (n : nat) (i : Int63.int) (acc : list byte) :=
+        match n with
+        | 0 => acc
+        | S n => go n (i - 1) (cons (i63_to_byte a.[i]) acc)
+        end) (nat_length a) (length a - 1) nil)%int63.
+
+  Definition from_byte_list (xs : list byte) :=
+    (let arr := make (list_length_i63 xs) 0 in
+    mk_intArray ((fix go i xs acc :=
+        match xs with
+        | nil => acc
+        | cons x xs => go (i + 1) xs (acc.[i <- i63_from_byte x])
+        end) 0 xs arr))%int63.
+
+  Declare Scope intArray_scope.
+  Delimit Scope intArray_scope with intArray.
+
+  String Notation intArray from_byte_list to_byte_list : intArray_scope.
+
+  Open Scope intArray_scope.
+  Check mk_intArray ( [| 97; 98; 99 | 0|])%int63%array.
+  Check "abc"%intArray.
+
+End Test2.
+
+(* Primitive arrays inside primitive arrays *)
+Module Test3.
+
+  Inductive nestArray := mk_nestArray (_ : array (array int)).
+  Definition to_byte_list '(mk_nestArray a) :=
+    ((fix go (n : nat) (i : Int63.int) (acc : list byte) :=
+        match n with
+        | 0 => acc
+        | S n => go n (i - 1) (cons (Test2.i63_to_byte a.[i].[0]) acc)
+        end) (Test2.nat_length a) (length a - 1) nil)%int63.
+
+  Definition from_byte_list (xs : list byte) :=
+    (let arr := make (Test2.list_length_i63 xs) (make 0 0) in
+    mk_nestArray ((fix go i xs acc :=
+        match xs with
+        | nil => acc
+        | cons x xs => go (i + 1) xs (acc.[i <- make 1 (Test2.i63_from_byte x)])
+        end) 0 xs arr))%int63.
+
+  Declare Scope nestArray_scope.
+  Delimit Scope nestArray_scope with nestArray.
+
+  String Notation nestArray from_byte_list to_byte_list : nestArray_scope.
+
+  Open Scope nestArray_scope.
+  Eval cbv in mk_nestArray ( [| make 1 97; make 1 98; make 1 99 | make 0 0|])%int63%array.
+  Check "abc"%nestArray.
+End Test3.
+
+
+
+(* Notations for primitive floats inside polymorphic datatypes *)
+Module Test4.
+  Import PrimFloat.
+  Inductive floatList := mk_floatList (_ : list float).
+  Definition float_from_byte (b : byte) : float :=
+    if Byte.eqb b "0"%byte then PrimFloat.zero else PrimFloat.one.
+  Definition float_to_byte (f : float) : byte :=
+    if PrimFloat.is_zero f then "0" else "1".
+  Definition to_byte_list '(mk_floatList a) := List.map float_to_byte a.
+
+  Definition from_byte_list (xs : list byte) : floatList:=
+    mk_floatList (List.map float_from_byte xs).
+
+  Declare Scope floatList_scope.
+  Delimit Scope floatList_scope with floatList.
+
+  String Notation floatList from_byte_list to_byte_list : floatList_scope.
+
+  Open Scope floatList_scope.
+  Import List.ListNotations.
+  Check mk_floatList [97; 0; 0]%float%list.
+  Check "100"%floatList.
+
+  Definition float' := float.
+  Check mk_floatList (@cons float' 1 [0; 0])%float%list.
+End Test4.