diff options
Diffstat (limited to 'parsing/extrawit.mli')
| -rw-r--r-- | parsing/extrawit.mli | 35 |
1 files changed, 8 insertions, 27 deletions
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli index c7795bb11..a74c8a259 100644 --- a/parsing/extrawit.mli +++ b/parsing/extrawit.mli @@ -15,33 +15,14 @@ open Tacexpr val tactic_main_level : int -val rawwit_tactic : int -> (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic : int -> (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic : int -> (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic0 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic0 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic0 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic1 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic1 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic1 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic2 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic2 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic2 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic3 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic3 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic3 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic4 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic4 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic4 : (glob_tactic_expr,tlevel) abstract_argument_type - -val rawwit_tactic5 : (raw_tactic_expr,rlevel) abstract_argument_type -val globwit_tactic5 : (glob_tactic_expr,glevel) abstract_argument_type -val wit_tactic5 : (glob_tactic_expr,tlevel) abstract_argument_type +val wit_tactic : int -> (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type + +val wit_tactic0 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type +val wit_tactic1 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type +val wit_tactic2 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type +val wit_tactic3 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type +val wit_tactic4 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type +val wit_tactic5 : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type val is_tactic_genarg : argument_type -> bool |