diff options
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 |