From 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 21:41:41 +0200
Subject: Creating a module Nameops.Name extending module Names.Name.

This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.

Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.

Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
---
 printing/ppconstr.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index f76555b047..60511d9138 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -151,8 +151,8 @@ let tag_var = tag Tag.variable
 
   let pr_univ l =
     match l with
-      | [_,x] -> pr_name x
-      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> pr_name (snd x)) l ++ str")"
+      | [_,x] -> Name.print x
+      | l -> str"max(" ++ prlist_with_sep (fun () -> str",") (fun x -> Name.print (snd x)) l ++ str")"
 
   let pr_univ_annot pr x = str "@{" ++ pr x ++ str "}"
 
@@ -166,7 +166,7 @@ let tag_var = tag Tag.variable
     | GProp -> tag_type (str "Prop")
     | GSet -> tag_type (str "Set")
     | GType None -> tag_type (str "Type")
-    | GType (Some (_, u)) -> tag_type (pr_name u)
+    | GType (Some (_, u)) -> tag_type (Name.print u)
 
   let pr_qualid sp =
     let (sl, id) = repr_qualid sp in
@@ -191,7 +191,7 @@ let tag_var = tag Tag.variable
       tag_type (str "Set")
     | GType u ->
       (match u with
-        | Some (_,u) -> pr_name u
+        | Some (_,u) -> Name.print u
         | None -> tag_type (str "Type"))
 
   let pr_universe_instance l =
@@ -224,7 +224,7 @@ let tag_var = tag Tag.variable
 
   let pr_lname = function
     | (loc,Name id) -> pr_lident (loc,id)
-    | lna -> pr_located pr_name lna
+    | lna -> pr_located Name.print lna
 
   let pr_or_var pr = function
     | ArgArg x -> pr x
-- 
cgit v1.2.3