diff options
Diffstat (limited to 'user-contrib/Ltac2/tac2core.ml')
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml index fa7df5dfeb..4758ecf5bd 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)) @@ -1744,6 +1754,16 @@ let () = add_scope "constr" (fun arg -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act) ) +let () = add_scope "open_constr" (fun arg -> + let delimiters = List.map (function + | SexprRec (_, { v = Some s }, []) -> s + | _ -> scope_fail "open_constr" arg) + arg + in + let act e = Tac2quote.of_open_constr ~delimiters e in + Tac2entries.ScopeRule (Pcoq.Symbol.nterm Pcoq.Constr.constr, act) + ) + let add_expr_scope name entry f = add_scope name begin function | [] -> Tac2entries.ScopeRule (Pcoq.Symbol.nterm entry, f) @@ -1772,7 +1792,6 @@ let () = add_expr_scope "constr_matching" q_constr_matching Tac2quote.of_constr_ let () = add_expr_scope "goal_matching" q_goal_matching Tac2quote.of_goal_matching let () = add_expr_scope "format" Pcoq.Prim.lstring Tac2quote.of_format -let () = add_generic_scope "open_constr" Pcoq.Constr.constr Tac2quote.wit_open_constr let () = add_generic_scope "pattern" Pcoq.Constr.constr Tac2quote.wit_pattern (** seq scope, a bit hairy *) |