From 1289b016fea5a54eb247cba1cac1fd9a19ee6d32 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 27 Apr 2016 22:13:02 +0200 Subject: Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"" This reverts commit eb9216e544cb5fce4347052f42e9452a822c2f64. --- interp/constrarg.mli | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'interp/constrarg.mli') diff --git a/interp/constrarg.mli b/interp/constrarg.mli index d38b1183c..b4029758a 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -71,6 +71,18 @@ val wit_red_expr : val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type +val wit_tactic0 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type + +val wit_tactic1 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type + +val wit_tactic2 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type + +val wit_tactic3 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type + +val wit_tactic4 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type + +val wit_tactic5 : (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. *) -- cgit v1.2.3