Merge PR#561: Improving the Name API

5 files changed, 18 insertions, 19 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4261573725..38c75fcf8c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -731,7 +731,7 @@ let get_names env sigma sign eqns =
 	     (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid))
 	     d na
 	 in
-         (na::l,(out_name na)::avoid))
+         (na::l,(Name.get_id na)::avoid))
       ([],allvars) (List.rev sign) names2 in
   names3,aliasname
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 752819aa39..6f099c8dfd 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -907,8 +907,7 @@ let simple_cases_matrix_of_branches ind brs =
       let nal,c = it_destRLambda_or_LetIn_names n b in
       let mkPatVar na = CAst.make @@ PatVar na in
       let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
-      let map name = try Some (Nameops.out_name name) with Failure _ -> None in
-      let ids = List.map_filter map nal in
+      let ids = List.map_filter Nameops.Name.to_option nal in
       Loc.tag @@ (ids,[p],c))
     brs
 
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 ->
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 578d365db3..6fb1b60898 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -210,20 +210,20 @@ let fold_glob_constr f acc = CAst.with_val (function
   )
 
 let fold_return_type_with_binders f g v acc (na,tyopt) =
-  Option.fold_left (f (name_fold g na v)) acc tyopt
+  Option.fold_left (f (Name.fold_right g na v)) acc tyopt
 
 let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function
   | GVar _ -> acc
   | GApp (c,args) -> List.fold_left (f v) (f v acc c) args
   | GLambda (na,_,b,c) | GProd (na,_,b,c) ->
-    f (name_fold g na v) (f v acc b) c
+    f (Name.fold_right g na v) (f v acc b) c
   | GLetIn (na,b,t,c) ->
-    f (name_fold g na v) (Option.fold_left (f v) (f v acc b) t) c
+    f (Name.fold_right g na v) (Option.fold_left (f v) (f v acc b) t) c
   | GCases (_,rtntypopt,tml,pl) ->
     let fold_pattern acc (_,(idl,p,c)) = f (List.fold_right g idl v) acc c in
     let fold_tomatch (v',acc) (tm,(na,onal)) =
-      (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (name_fold g) nal v'')
-                        (name_fold g na v') onal,
+      (Option.fold_left (fun v'' (_,(_,nal)) -> List.fold_right (Name.fold_right g) nal v'')
+                        (Name.fold_right g na v') onal,
        f v acc tm) in
     let (v',acc) = List.fold_left fold_tomatch (v,acc) tml in
     let acc = Option.fold_left (f v') acc rtntypopt in
@@ -237,7 +237,7 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function
       let v,acc =
 	List.fold_left
 	  (fun (v,acc) (na,k,bbd,bty) ->
-            (name_fold g na v, f v (Option.fold_left (f v) acc bbd) bty))
+            (Name.fold_right g na v, f v (Option.fold_left (f v) acc bbd) bty))
           (v,acc)
           bll.(i) in
       f (Array.fold_right g idl v) (f v acc tyl.(i)) (bv.(i)) in
@@ -366,12 +366,12 @@ let loc_of_glob_constr c = c.CAst.loc
 
 let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l
 let test_id l id = if collide_id l id then raise Not_found
-let test_na l na = name_iter (test_id l) na
+let test_na l na = Name.iter (test_id l) na
 
 let update_subst na l =
   let in_range id l = List.exists (fun (_,id') -> Id.equal id id') l in
-  let l' = name_fold Id.List.remove_assoc na l in
-  name_fold
+  let l' = Name.fold_right Id.List.remove_assoc na l in
+  Name.fold_right
     (fun id _ ->
      if in_range id l' then
        let id' = Namegen.next_ident_away_from id (fun id' -> in_range id' l') in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 1c8ad0cddd..0818a55256 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -340,15 +340,15 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
   | GLambda (na,bk,c1,c2) ->
-      name_iter (fun n -> metas := n::!metas) na;
+      Name.iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
   | GProd (na,bk,c1,c2) ->
-      name_iter (fun n -> metas := n::!metas) na;
+      Name.iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
   | GLetIn (na,c1,t,c2) ->
-      name_iter (fun n -> metas := n::!metas) na;
+      Name.iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
                Option.map (pat_of_raw metas vars) t,
 	       pat_of_raw metas (na::vars) c2)
@@ -411,7 +411,7 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
 and pats_of_glob_branches loc metas vars ind brs =
   let get_arg = function
     | { CAst.v = PatVar na } ->
-      name_iter (fun n -> metas := n::!metas) na;
+      Name.iter (fun n -> metas := n::!metas) na;
       na
     | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.")
   in