diff options
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/Ltac1.v | 3 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 10 |
2 files changed, 13 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v index fd1555c2fb..0f7167939b 100644 --- a/user-contrib/Ltac2/Ltac1.v +++ b/user-contrib/Ltac2/Ltac1.v @@ -40,5 +40,8 @@ Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "ltac2" "ltac1_ap Ltac2 @ external of_constr : constr -> t := "ltac2" "ltac1_of_constr". Ltac2 @ external to_constr : t -> constr option := "ltac2" "ltac1_to_constr". +Ltac2 @ external of_ident : ident -> t := "ltac2" "ltac1_of_ident". +Ltac2 @ external to_ident : t -> ident option := "ltac2" "ltac1_to_ident". + Ltac2 @ external of_list : t list -> t := "ltac2" "ltac1_of_list". Ltac2 @ external to_list : t -> t list option := "ltac2" "ltac1_to_list". diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index fa7df5dfeb..457b8e1acf 100644 --- a/user-contrib/Ltac2/tac2core.ml +++ b/user-contrib/Ltac2/tac2core.ml @@ -1186,6 +1186,16 @@ let () = define1 "ltac1_to_constr" ltac1 begin fun v -> return (Value.of_option Value.of_constr (Tacinterp.Value.to_constr v)) end +let () = define1 "ltac1_of_ident" ident begin fun c -> + let open Ltac_plugin in + return (Value.of_ext val_ltac1 (Taccoerce.Value.of_ident c)) +end + +let () = define1 "ltac1_to_ident" ltac1 begin fun v -> + let open Ltac_plugin in + return (Value.of_option Value.of_ident (Taccoerce.Value.to_ident v)) +end + let () = define1 "ltac1_of_list" (list ltac1) begin fun l -> let open Geninterp.Val in return (Value.of_ext val_ltac1 (inject (Base typ_list) l)) |