diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 8557953cc4..5828e7f433 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -129,7 +129,7 @@ let pattern_of_constr sigma t = | Var id -> PVar id | Sort (Prop Null) -> PSort GProp | Sort (Prop Pos) -> PSort GSet - | Sort (Type _) -> PSort (GType None) + | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr c | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b) | Prod (na,c,b) -> PProd (na,pattern_of_constr c,pattern_of_constr b) |