diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-09-08 10:23:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-09-08 17:09:43 +0200 |
| commit | 26a79004e47bbdc97df61015ce7e944eef14ac71 (patch) | |
| tree | 1f24c9acbb73cd63dcc689222b965f245767137e /pretyping/patternops.ml | |
| parent | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (diff) | |
Parsing of Type@{max(i,j)}.
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 8557953cc..5828e7f43 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) |