9 files changed, 80 insertions, 23 deletions
diff --git a/test-suite/bugs/closed/bug_9684.v b/test-suite/bugs/closed/bug_9684.v
new file mode 100644
index 0000000000..436a00585b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9684.v
@@ -0,0 +1,19 @@
+Set Primitive Projections.
+
+Record foo := mkFoo { proj1 : bool; proj2 : bool }.
+
+Definition x := mkFoo true false.
+Definition proj x := proj2 x.
+
+Lemma oops : proj = fun x => proj1 x.
+Proof. Fail native_compute; reflexivity. Abort.
+
+(*
+Lemma bad : False.
+assert (proj1 x = proj x).
+  rewrite oops; reflexivity.
+discriminate.
+Qed.
+
+Print Assumptions bad.
+*)
diff --git a/test-suite/coq-makefile/missing-install/run.sh b/test-suite/coq-makefile/missing-install/run.sh
new file mode 100755
index 0000000000..4f36fdcb1c
--- /dev/null
+++ b/test-suite/coq-makefile/missing-install/run.sh
@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+. ../template/init.sh
+
+rm -rf _test; mkdir _test; cd _test
+
+cat > _CoqProject <<EOF
+-R theories Test
+theories/a.v
+theories/b.v
+EOF
+mkdir theories
+touch theories/a.v theories/b.v
+
+coq_makefile -f _CoqProject -o Makefile
+make theories/b.vo
+if make install; then exit 1; fi
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 78a3f7c63a..4ee4aae36c 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -49,16 +49,15 @@ TO_SED_IN_BOTH=(
     -e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out
     -e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators
     -e s'/+/-/g' # some code lines don't really change, but this can show up as either -0m00.01s or +0m00.01s, so we need to normalize the signs; additionally, some N/A's show up where we expect to get -∞ on the per-line file, and so the ∞-replacement gets the sign wrong, so we must correct it
+    -e s'/[0-9]//g' # sometimes the time is under 1 minute, sometimes it's over 1 minute, so we want to remove/normalize both instances; see https://github.com/coq/coq/issues/5675#issuecomment-487378622
 )
 
 TO_SED_IN_PER_FILE=(
-    -e s'/[0-9]//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
     -e s'/  */ /g' # unclear whether this is actually needed for per-file timing; it's been here from the start
     -e s'/\(Total.*\)-\(.*\)-/\1+\2+/g' # Overall time in the per-file timing diff should be around 0; if it comes out negative, we remove the sign
 )
 
 TO_SED_IN_PER_LINE=(
-    -e s'/0//g' # unclear whether this is actually needed above and beyond s'/[0-9]*\.[0-9]*//g'; it's been here from the start
     -e s'/  */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
     )
 
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index fdd5599565..4d76f1210b 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -1,3 +1,7 @@
+2%int63
+     : int
+(2 + 2)%int63
+     : int
 2
      : int
 9223372036854775807
@@ -14,3 +18,15 @@ The command has indeed failed with message:
 int63 are only non-negative numbers.
 The command has indeed failed with message:
 overflow in int63 literal: 9223372036854775808
+2
+     : nat
+2%int63
+     : int
+t = 2%i63
+     : int
+t = 2%i63
+     : int
+2
+     : nat
+2
+     : int
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index 3dc364eddb..0385e529bf 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -1,5 +1,7 @@
 Require Import Int63 Cyclic63.
 
+Check 2%int63.
+Check (2 + 2)%int63.
 Open Scope int63_scope.
 Check 2.
 Check 9223372036854775807.
@@ -9,4 +11,15 @@ Eval vm_compute in 2+2.
 Eval vm_compute in 65675757 * 565675998.
 Fail Check -1.
 Fail Check 9223372036854775808.
+Open Scope nat_scope.
+Check 2. (* : nat *)
+Check 2%int63.
+Delimit Scope int63_scope with i63.
+Definition t := 2%int63.
+Print t.
+Delimit Scope nat_scope with int63.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
 Close Scope int63_scope.
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index cb49e66ed7..460c77879c 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -82,10 +82,6 @@ function (of_uint) targets an option type.
 The command has indeed failed with message:
 The 'abstract after' directive has no effect when the parsing function
 (of_uint) targets an option type. [abstract-large-number-no-op,numbers]
-The command has indeed failed with message:
-The reference of_uint was not found in the current environment.
-The command has indeed failed with message:
-The reference of_uint was not found in the current environment.
 let v := of_uint (Decimal.D1 Decimal.Nil) in v : unit
      : unit
 let v := 0%test13 in v : unit
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index fcfdd82dcc..44805ad09d 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -207,21 +207,6 @@ Module Test10.
   Numeral Notation unit of_any_uint to_uint : unit2_scope (abstract after 1).
 End Test10.
 
-Module Test11.
-  (* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
-  Inductive unit11 := tt11.
-  Declare Scope unit11_scope.
-  Delimit Scope unit11_scope with unit11.
-  Goal True.
-    evar (to_uint : unit11 -> Decimal.uint).
-    evar (of_uint : Decimal.uint -> unit11).
-    Fail Numeral Notation unit11 of_uint to_uint : uint11_scope.
-    exact I.
-    Unshelve.
-    all: solve [ constructor ].
-  Qed.
-End Test11.
-
 Module Test12.
   (* Test for numeral notations on context variables *)
   Declare Scope test12_scope.
diff --git a/test-suite/success/NumeralNotationsNoLocal.v b/test-suite/success/NumeralNotationsNoLocal.v
new file mode 100644
index 0000000000..ea3907ef8a
--- /dev/null
+++ b/test-suite/success/NumeralNotationsNoLocal.v
@@ -0,0 +1,12 @@
+(* Test that numeral notations don't work on proof-local variables, especially not ones containing evars *)
+Inductive unit11 := tt11.
+Declare Scope unit11_scope.
+Delimit Scope unit11_scope with unit11.
+Goal True.
+  evar (to_uint : unit11 -> Decimal.uint).
+  evar (of_uint : Decimal.uint -> unit11).
+  Fail Numeral Notation unit11 of_uint to_uint : uint11_scope.
+  exact I.
+  Unshelve.
+  all: solve [ constructor ].
+Qed.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 85d7a770fc..02adb012d9 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -13,7 +13,7 @@ Print sigT_rect.
 Obligation Tactic := program_simplify ; auto with *.
 About MR.
 
-Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat :=
+Program Fixpoint merge (n m : nat) {measure (n + m) lt} : nat :=
   match n with
     | 0 => 0
     | S n' => merge n' m
@@ -101,5 +101,5 @@ Next Obligation. simpl in *; intros.
 Qed.
 
 Program Fixpoint check_n'  (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p})
-  {measure (p - n) p} : nat :=
+  {measure (p - n)} : nat :=
   _.