Merge PR #8988: Towards unifying parsing/printing for universe instances and Type's argument

Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes

1 files changed, 8 insertions, 9 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fe50bd4b08..701c07dc8d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -757,11 +757,10 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
 (* mapping glob_constr to constr_expr                                    *)
 
 let extern_glob_sort = function
-  | GSProp -> GSProp
-  | GProp -> GProp
-  | GSet -> GSet
-  | GType _ as s when !print_universes -> s
-  | GType _ -> GType []
+  (* In case we print a glob_constr w/o having passed through detyping *)
+  | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u
+  | UNamed _ when not !print_universes -> UAnonymous {rigid=true}
+  | UNamed _ | UAnonymous _ as u -> u
 
 let extern_universes = function
   | Some _ as l when !print_universes -> l
@@ -1312,10 +1311,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
           Array.map (fun (bl,_,_) -> bl) v,
           Array.map (fun (_,_,ty) -> ty) v,
           Array.map (fun (_,bd,_) -> bd) v)
-  | PSort Sorts.InSProp -> GSort GSProp
-  | PSort Sorts.InProp -> GSort GProp
-  | PSort Sorts.InSet -> GSort GSet
-  | PSort Sorts.InType -> GSort (GType [])
+  | PSort Sorts.InSProp -> GSort (UNamed [GSProp,0])
+  | PSort Sorts.InProp -> GSort (UNamed [GProp,0])
+  | PSort Sorts.InSet -> GSort (UNamed [GSet,0])
+  | PSort Sorts.InType -> GSort (UAnonymous {rigid=true})
   | PInt i -> GInt i
 
 let extern_constr_pattern env sigma pat =