diff options
Diffstat (limited to 'pretyping/pattern.mli')
| -rw-r--r-- | pretyping/pattern.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index b25637de9e..23de675989 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -70,7 +70,7 @@ type constr_pattern = | PLambda of name * constr_pattern * constr_pattern | PProd of name * constr_pattern * constr_pattern | PLetIn of name * constr_pattern * constr_pattern - | PSort of rawsort + | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of (case_style * int array * inductive option * (int * int) option) |