diff options
Diffstat (limited to 'plugins/decl_mode/decl_expr.mli')
| -rw-r--r-- | plugins/decl_mode/decl_expr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 966ebff40..5b7f0b4c7 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -11,7 +11,7 @@ open Pp open Tacexpr type 'it statement = - {st_label:name; + {st_label:Name.t; st_it:'it} type thesis_kind = |