11 files changed, 101 insertions, 23 deletions
diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v
index 9c11d19c27..b50371386f 100644
--- a/test-suite/ltac2/compat.v
+++ b/test-suite/ltac2/compat.v
@@ -40,6 +40,67 @@ Fail Ltac1.run (ltac1val:(x |- idtac) 0).
 Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))).
 Abort.
 
+(** Check value-returning FFI *)
+
+(* A dummy CPS wrapper in Ltac1 *)
+Ltac arg k :=
+match goal with
+| [ |- ?P ] => k P
+end.
+
+Ltac2 testeval v :=
+  let r := { contents := None } in
+  let k c :=
+    let () := match Ltac1.to_constr c with
+    | None => ()
+    | Some c => r.(contents) := Some c
+    end in
+    (* dummy return value *)
+    ltac1val:(idtac)
+  in
+  let tac := ltac1val:(arg) in
+  let () := Ltac1.apply tac [Ltac1.lambda k] (fun _ => ()) in
+  match r.(contents) with
+  | None => fail
+  | Some c => if Constr.equal v c then () else fail
+  end.
+
+Goal True.
+Proof.
+testeval 'True.
+Abort.
+
+Goal nat.
+Proof.
+testeval 'nat.
+Abort.
+
+(* CPS towers *)
+Ltac2 testeval2 tac :=
+  let fail _ := Control.zero Not_found in
+  let cast c := match Ltac1.to_constr c with
+  | None => fail ()
+  | Some c => c
+  end in
+  let f x y z :=
+    let x := cast x in
+    let y := cast y in
+    let z := cast z in
+    Ltac1.of_constr constr:($x $y $z)
+  in
+  let f := Ltac1.lambda (fun x => Ltac1.lambda (fun y => Ltac1.lambda (fun z => f x y z))) in
+  Ltac1.apply tac [f] Ltac1.run.
+
+Goal False -> True.
+Proof.
+ltac1:(
+let ff := ltac2:(tac |- testeval2 tac) in
+ff ltac:(fun k =>
+  let c := k (fun (n : nat) (i : True) (e : False) => i) O I in
+  exact c)
+).
+Qed.
+
 (** Test calls to Ltac2 from Ltac1 *)
 
 Set Default Proof Mode "Classic".
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index eefa338f0d..ca8e1b58a8 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -1,7 +1,5 @@
 2%int63
      : int
-(2 + 2)%int63
-     : int
 2
      : int
 9223372036854775807
@@ -17,9 +15,9 @@
 427
      : int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
 The command has indeed failed with message:
-Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.Int63.int
+Cannot interpret this number as a value of type Coq.Numbers.Cyclic.Int63.PrimInt63.int
 0
      : int
 0
@@ -32,13 +30,7 @@ The command has indeed failed with message:
 The reference x1 was not found in the current environment.
 The command has indeed failed with message:
 The reference x was not found in the current environment.
-2 + 2
-     : int
-2 + 2
-     : int
-     = 4
-     : int
-     = 37151199385380486
+add 2 2
      : int
 The command has indeed failed with message:
 int63 are only non-negative numbers.
@@ -56,3 +48,11 @@ t = 2%i63
      : nat
 2
      : int
+(2 + 2)%int63
+     : int
+2 + 2
+     : int
+     = 4
+     : int
+     = 37151199385380486
+     : int
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v
index c49616d918..6f1046f7a5 100644
--- a/test-suite/output/Int63Syntax.v
+++ b/test-suite/output/Int63Syntax.v
@@ -1,7 +1,6 @@
-Require Import Int63 Cyclic63.
+Require Import PrimInt63.
 
 Check 2%int63.
-Check (2 + 2)%int63.
 Open Scope int63_scope.
 Check 2.
 Check 9223372036854775807.
@@ -18,10 +17,7 @@ Fail Check 0xg.
 Fail Check 0xG.
 Fail Check 00x1.
 Fail Check 0x.
-Check (Int63.add 2 2).
-Check (2+2).
-Eval vm_compute in 2+2.
-Eval vm_compute in 65675757 * 565675998.
+Check (PrimInt63.add 2 2).
 Fail Check -1.
 Fail Check 9223372036854775808.
 Open Scope nat_scope.
@@ -36,3 +32,11 @@ Check 2.
 Close Scope nat_scope.
 Check 2.
 Close Scope int63_scope.
+
+Require Import Int63.
+
+Check (2 + 2)%int63.
+Open Scope int63_scope.
+Check (2+2).
+Eval vm_compute in 2+2.
+Eval vm_compute in 65675757 * 565675998.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 0fbb4f4c11..95b6c6ee95 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -162,6 +162,9 @@ When declaring multiple axioms in one command, only the first is allowed a unive
 foo@{i} = Type@{M.i} -> Type@{i}
      : Type@{max(M.i+1,i+1)}
 (* i |=  *)
+Type@{u0} -> Type@{UnivBinders.64}
+     : Type@{max(u0+1,UnivBinders.64+1)}
+(* {UnivBinders.64} |=  *)
 bind_univs.mono = 
 Type@{bind_univs.mono.u}
      : Type@{bind_univs.mono.u+1}
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index ed6e90b2a6..9539e34cfe 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -161,6 +161,16 @@ Module Notas.
 
 End Notas.
 
+Module NoAutoNames.
+  Monomorphic Universe u0.
+
+  (* The anonymous universe doesn't get a name (names are only
+     invented at the end of a definition/inductive) so no need to
+     qualify u0. *)
+  Check (Type@{u0} -> Type).
+
+End NoAutoNames.
+
 (* Universe binders survive through compilation, sections and modules. *)
 Require TestSuite.bind_univs.
 Print bind_univs.mono.
diff --git a/test-suite/primitive/uint63/addcarryc.v b/test-suite/primitive/uint63/addcarryc.v
index a4430769ca..7ab3af51d8 100644
--- a/test-suite/primitive/uint63/addcarryc.v
+++ b/test-suite/primitive/uint63/addcarryc.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v
index 72b0164b49..e3aded6c96 100644
--- a/test-suite/primitive/uint63/addmuldiv.v
+++ b/test-suite/primitive/uint63/addmuldiv.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/diveucl.v b/test-suite/primitive/uint63/diveucl.v
index 8f88a0f356..43a0741ffe 100644
--- a/test-suite/primitive/uint63/diveucl.v
+++ b/test-suite/primitive/uint63/diveucl.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/head0.v b/test-suite/primitive/uint63/head0.v
index f4234d2605..30cbce4537 100644
--- a/test-suite/primitive/uint63/head0.v
+++ b/test-suite/primitive/uint63/head0.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/subcarryc.v b/test-suite/primitive/uint63/subcarryc.v
index e81b6536b2..6a773dde5d 100644
--- a/test-suite/primitive/uint63/subcarryc.v
+++ b/test-suite/primitive/uint63/subcarryc.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.
 
diff --git a/test-suite/primitive/uint63/tail0.v b/test-suite/primitive/uint63/tail0.v
index c9d426087a..1f91e4106c 100644
--- a/test-suite/primitive/uint63/tail0.v
+++ b/test-suite/primitive/uint63/tail0.v
@@ -1,4 +1,4 @@
-Require Import Int63.
+Require Import PrimInt63.
 
 Set Implicit Arguments.