diff options
| -rw-r--r-- | interp/constrarg.ml | 2 | ||||
| -rw-r--r-- | interp/constrarg.mli | 5 | ||||
| -rw-r--r-- | parsing/pcoq.ml | 1 | ||||
| -rw-r--r-- | printing/pptactic.ml | 5 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
7 files changed, 19 insertions, 0 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 81e942d82..46be0b8a1 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -28,6 +28,8 @@ let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = Genarg.make0 "tactic" +let wit_ltac = Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac" + let wit_ident = Genarg.make0 "ident" diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 1197b85a2..d38b1183c 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -71,6 +71,11 @@ val wit_red_expr : val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type +(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their + toplevel interpretation. The one of [wit_ltac] forces the tactic and + discards the result. *) +val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type + val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type (** Aliases for compatibility *) diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index c7cb62d59..207b43064 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -881,5 +881,6 @@ let () = (* Grammar.register0 wit_hyp_location_flag; *) Grammar.register0 wit_red_expr (Tactic.red_expr); Grammar.register0 wit_tactic (Tactic.tactic); + Grammar.register0 wit_ltac (Tactic.tactic); Grammar.register0 wit_clause_dft_concl (Tactic.clause_dft_concl); () diff --git a/printing/pptactic.ml b/printing/pptactic.ml index d99a5f0d8..982c18ec6 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -1415,6 +1415,11 @@ let () = let printer _ _ prtac = prtac (0, E) in declare_extra_genarg_pprule wit_tactic printer printer printer +let () = + let pr_unit _ _ _ () = str "()" in + let printer _ _ prtac = prtac (0, E) in + declare_extra_genarg_pprule wit_ltac printer printer pr_unit + module Richpp = struct include Make (Ppconstr.Richpp) (struct diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 89dc843cb..a75805b4f 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -795,6 +795,7 @@ let () = Genintern.register_intern0 wit_ident intern_ident'; Genintern.register_intern0 wit_var (lift intern_hyp); Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg); + Genintern.register_intern0 wit_ltac (lift intern_tactic_or_tacarg); Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)); Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); Genintern.register_intern0 wit_constr (fun ist c -> (ist,intern_constr ist c)); diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 5dab244af..8afc73526 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2144,6 +2144,10 @@ let () = Geninterp.register_interp0 wit_tactic interp let () = + let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in + Geninterp.register_interp0 wit_ltac interp + +let () = Geninterp.register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c) end }) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 55941c1ca..4059877b7 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -299,6 +299,7 @@ let () = Genintern.register_subst0 wit_var (fun _ v -> v); Genintern.register_subst0 wit_intro_pattern (fun _ v -> v); Genintern.register_subst0 wit_tactic subst_tactic; + Genintern.register_subst0 wit_ltac subst_tactic; Genintern.register_subst0 wit_constr subst_glob_constr; Genintern.register_subst0 wit_sort (fun _ v -> v); Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v); |