diff options
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 8 | ||||
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
2 files changed, 1 insertions, 9 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 719cf0d33b..dbe8887149 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -270,15 +270,7 @@ type raw_tactic_arg = (** Misc *) -type raw_generic_argument = rlevel generic_argument -type glob_generic_argument = glevel generic_argument -type typed_generic_argument = tlevel generic_argument - type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen type glob_red_expr = (g_trm, g_cst, g_pat) red_expr_gen -type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type -type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type -type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type - type 'a declaration_hook = locality -> global_reference -> 'a diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index b311b770db..138ef5cbbe 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -398,7 +398,7 @@ type vernac_expr = | VernacToplevelControl of exn (* For extension *) - | VernacExtend of string * raw_generic_argument list + | VernacExtend of string * Genarg.raw_generic_argument list (* Flags *) | VernacProgram of vernac_expr |