1 files changed, 61 insertions, 0 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".