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 6c6dbf0f60..fa6acaeb1f 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -93,7 +93,7 @@ type proof_pattern = pat_aliases: (Term.constr*Term.types) statement list; pat_constr: Term.constr; pat_typ: Term.types; - pat_pat: Rawterm.cases_pattern; + pat_pat: Glob_term.cases_pattern; pat_expr: Topconstr.cases_pattern_expr} type proof_instr = |