diff options
Diffstat (limited to 'plugins/ltac/tacarg.ml')
| -rw-r--r-- | plugins/ltac/tacarg.ml | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 6eb482b1..8a25d485 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -19,6 +19,14 @@ let make0 ?dyn name = let () = Geninterp.register_val0 wit dyn in wit +let wit_intro_pattern = make0 "intropattern" +let wit_quant_hyp = make0 "quant_hyp" +let wit_constr_with_bindings = make0 "constr_with_bindings" +let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" +let wit_bindings = make0 "bindings" +let wit_quantified_hypothesis = wit_quant_hyp +let wit_intropattern = wit_intro_pattern + let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = make0 "tactic" |