diff options
| author | Pierre-Marie Pédrot | 2019-03-20 09:25:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-20 09:25:29 +0100 |
| commit | b899b102e071ba0faa07949b2ee66bbb7dade23b (patch) | |
| tree | dacdbac86eafb367d5a865f040b70343cb80a1a2 /pretyping/pattern.ml | |
| parent | e5a2f0452cf9523bc86e71ae6d2ac30883a28be6 (diff) | |
| parent | a71f586e23b0e68032c556bfa1c37df8f4358c71 (diff) | |
Merge PR #9791: Fix constr_matching on SProp
Ack-by: SkySkimmer
Reviewed-by: ppedrot
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 * |