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.
---
 pretyping/evarconv.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/evarconv.ml')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index bf62cea6b6..630f80ad2f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -638,7 +638,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	     (fun i ->
 	       let b = nf_evar i b1 in
 	       let t = nf_evar i t1 in
-               let na = Nameops.name_max na1 na2 in
+               let na = Nameops.Name.pick na1 na2 in
 	       evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2);
 	     (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
 	and f2 i =
@@ -755,7 +755,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
           [(fun i -> evar_conv_x ts env i CONV c1 c2);
            (fun i ->
 	     let c = nf_evar i c1 in
-             let na = Nameops.name_max na1 na2 in
+             let na = Nameops.Name.pick na1 na2 in
 	     evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)]
 
     | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2
@@ -816,7 +816,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
               [(fun i -> evar_conv_x ts env i CONV c1 c2);
                (fun i ->
  	         let c = nf_evar i c1 in
-                 let na = Nameops.name_max n1 n2 in
+                 let na = Nameops.Name.pick n1 n2 in
 	         evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)]
 
 	| Rel x1, Rel x2 ->
-- 
cgit v1.2.3