4 files changed, 48 insertions, 2 deletions
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/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/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 :=
   _.