diff options
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 943a8d8c3..4b8c0aa8d 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -29,7 +29,8 @@ type constr_pattern = | PLetIn of name * constr_pattern * constr_pattern | PSort of Rawterm.rawsort | PMeta of int option - | PCase of constr_pattern option * constr_pattern * constr_pattern array + | PCase of case_style * constr_pattern option * constr_pattern * + constr_pattern array | PFix of fixpoint | PCoFix of cofixpoint |