Add Ltac2.Ltac1.to/of_int

plugins/ltac2_ltac1/tac2core_ltac1.ml

@@ -73,6 +73,14 @@ let () =
   let tac = CAst.make @@ TacArg (TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
   Tacinterp.val_interp ist tac k
 
+let () =
+  define "ltac1_of_int" (int @-> ret ltac1)
+    Ltac_plugin.Tacinterp.Value.of_int
+
+let () =
+  define "ltac1_to_int" (ltac1 @-> ret (option int))
+    Ltac_plugin.Tacinterp.Value.to_int
+
 let () =
   define "ltac1_of_constr" (constr @-> ret ltac1)
     Ltac_plugin.Tacinterp.Value.of_constr

test-suite/ltac2/ltac1_conversions.v

@@ -28,4 +28,29 @@ Goal nat. (* we need an open goal because ltac1 auto focuses *)
     | _ => Control.throw Assertion_failure
     end.
 
+  Ltac2 Eval
+    ltac1:(
+      let n := numgoals in
+      let t := ltac2:(n |-
+        match Ltac1.to_int n with
+        | Some 1 => ()
+        | _ => Control.throw Assertion_failure
+        end)
+      in
+      t n).
+
+  Fail Ltac2 Eval
+    ltac1:(
+      let n := numgoals in
+      let t := ltac2:(n |-
+        match Ltac1.to_int n with
+        | None => ()
+        | _ => Control.throw Assertion_failure
+        end)
+      in
+      t n).
+
+  Ltac2 Eval
+   ltac1:(n |- do n assert False; [| | |]) (Ltac1.of_int 2).
+
 Abort.

user-contrib/Ltac2/Ltac1.v

@@ -37,6 +37,11 @@ Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "coq-core.plugins
 
 (** Conversion functions *)
 
+Ltac2 @ external of_int : int -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_int".
+(** Converts an Ltac2 int into an Ltac1 value. *)
+Ltac2 @ external to_int : t -> int option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_int".
+(** Converts an Ltac1 int into an Ltac2 value. *)
+
 Ltac2 @ external of_constr : constr -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_constr".
 (** Converts an Ltac2 constr into an Ltac1 value. *)
 Ltac2 @ external to_constr : t -> constr option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_constr".