1 files changed, 9 insertions, 9 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 10a7a4158b..811abd67f9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -301,8 +301,8 @@ let constr_display csr =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ())
 
   and sort_display = function
-    | Prop(Pos) -> "Prop(Pos)"
-    | Prop(Null) -> "Prop(Null)"
+    | Set -> "Set"
+    | Prop -> "Prop"
     | Type u -> univ_display u;
 	"Type("^(string_of_int !cnt)^")"
 
@@ -423,8 +423,8 @@ let print_pure_constr csr =
     Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u)
 
   and sort_display = function
-    | Prop(Pos) -> print_string "Set"
-    | Prop(Null) -> print_string "Prop"
+    | Set -> print_string "Set"
+    | Prop -> print_string "Prop"
     | Type u -> open_hbox();
 	print_string "Type("; pp (pr_uni u); print_string ")"; close_box()
 
@@ -549,8 +549,8 @@ let encode_path ?loc prefix mpdir suffix id =
     | Some (mp,dir) ->
 	(DirPath.repr (dirpath_of_string (ModPath.to_string mp))@
 	DirPath.repr dir) in
-  CAst.make ?loc @@ Qualid (make_qualid
-    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id)
+  make_qualid ?loc
+    (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id
 
 let raw_string_of_ref ?loc _ = function
   | ConstRef cst ->
@@ -569,9 +569,9 @@ let raw_string_of_ref ?loc _ = function
       encode_path ?loc "SECVAR" None [] id
 
 let short_string_of_ref ?loc _ = function
-  | VarRef id -> CAst.make ?loc @@ Ident id
-  | ConstRef cst -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (Constant.repr3 cst)))
-  | IndRef (kn,0) -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (MutInd.repr3 kn)))
+  | VarRef id -> qualid_of_ident ?loc id
+  | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst)))
+  | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn)))
   | IndRef (kn,i) ->
       encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))]
         (Id.of_string ("_"^string_of_int i))