diff options
| author | Matthieu Sozeau | 2014-09-08 10:23:12 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-08 17:09:43 +0200 |
| commit | 26a79004e47bbdc97df61015ce7e944eef14ac71 (patch) | |
| tree | 1f24c9acbb73cd63dcc689222b965f245767137e /interp/constrextern.ml | |
| parent | 89ad50f4d7e1312539995ced3a632821bf6af7c5 (diff) | |
Parsing of Type@{max(i,j)}.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 36fa81157a..d51d067b28 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -595,8 +595,8 @@ let extern_optimal_prim_token scopes r r' = let extern_glob_sort = function | GProp -> GProp | GSet -> GSet - | GType (Some _) as s when !print_universes -> s - | GType _ -> GType None + | GType _ as s when !print_universes -> s + | GType _ -> GType [] let extern_universes = function | Some _ as l when !print_universes -> l |