From 26a79004e47bbdc97df61015ce7e944eef14ac71 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 8 Sep 2014 10:23:12 +0200 Subject: Parsing of Type@{max(i,j)}. --- pretyping/patternops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/patternops.ml') 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) -- cgit v1.2.3