From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/ltac/tacarg.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'plugins/ltac/tacarg.ml') 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" -- cgit v1.2.3