diff options
| author | Gaëtan Gilbert | 2019-03-17 10:40:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-18 12:52:42 +0100 |
| commit | a71f586e23b0e68032c556bfa1c37df8f4358c71 (patch) | |
| tree | 876772675b8bcf7cfa3d4ff2b7ea460c62ebd04f /pretyping/pattern.ml | |
| parent | 9ac5483132b42e845a0708491843693b70893eef (diff) | |
Fix constr_matching on SProp
Diffstat (limited to 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 2ca7f21e8d..d1c0a4ea2a 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -32,7 +32,7 @@ type constr_pattern = | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern - | PSort of Glob_term.glob_sort + | PSort of Sorts.family | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern | PCase of case_info_pattern * constr_pattern * constr_pattern * |