Merge PR#561: Improving the Name API

5 files changed, 28 insertions, 28 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 4c29fc8097..f6da10c961 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -740,7 +740,7 @@ let rec extern inctx scopes vars r =
 
   | GCases (sty,rtntypopt,tml,eqns) ->
     let vars' =
-      List.fold_right (name_fold Id.Set.add)
+      List.fold_right (Name.fold_right Id.Set.add)
 	(cases_predicate_names tml) vars in
     let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
     let tml = List.map (fun (tm,(na,x)) ->
@@ -790,12 +790,12 @@ let rec extern inctx scopes vars r =
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
                  let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
-                 let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
-                 let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
+                 let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
+                 let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
 		 let n =
 		   match fst nv.(i) with
 		     | None -> None
-		     | Some x -> Some (Loc.tag @@ out_name (List.nth assums x))
+		     | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x))
 		 in
 		 let ro = extern_recursion_order scopes vars (snd nv.(i)) in
 		 ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty,
@@ -807,8 +807,8 @@ let rec extern inctx scopes vars r =
                Array.mapi (fun i fi ->
                  let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in
                  let (_,ids,bl) = extern_local_binder scopes vars bl in
-                 let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
-                 let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
+                 let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
+                 let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
 		 ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern false scopes vars1 bv.(i))) idv
 	     in
@@ -852,14 +852,14 @@ and extern_local_binder scopes vars = function
     [] -> ([],[],[])
   | { v = GLocalDef (na,bk,bd,ty)}::l ->
       let (assums,ids,l) =
-        extern_local_binder scopes (name_fold Id.Set.add na vars) l in
+        extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in
       (assums,na::ids,
        CLocalDef((Loc.tag na), extern false scopes vars bd,
                    Option.map (extern false scopes vars) ty) :: l)
 
   | { v = GLocalAssum (na,bk,ty)}::l ->
       let ty = extern_typ scopes vars ty in
-      (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
+      (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with
           (assums,ids,CLocalAssum(nal,k,ty')::l)
             when constr_expr_eq ty ty' &&
               match na with Name id -> not (occur_var_constr_expr id ty')
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6514ad8be5..81ebf65610 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -536,7 +536,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
   try
     (* Binders bound in the notation are considered first-order objects *)
     let _,na = coerce_to_name (fst (Id.Map.find id terms)) in
-    (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na
+    (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
@@ -1660,7 +1660,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
     | CCases (sty, rtnpo, tms, eqns) ->
         let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
 	  Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
-            (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na)
+            (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na)
 	    inb) Id.Set.empty tms in
         (* as, in & return vars *)
         let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
@@ -2071,7 +2071,7 @@ let intern_context global_level env impl_env binders =
   with InternalizationError (loc,e) ->
     user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
 
-let interp_rawcontext_evars env evdref k bl =
+let interp_glob_context_evars env evdref k bl =
   let open EConstr in
   let (env, par, _, impls) =
     List.fold_left
@@ -2100,6 +2100,6 @@ let interp_rawcontext_evars env evdref k bl =
 
 let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params =
   let int_env,bl = intern_context global_level env impl_env params in
-  let x = interp_rawcontext_evars env evdref shift bl in
+  let x = interp_glob_context_evars env evdref shift bl in
   int_env, x
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index cfc6e6c2a6..ade524141a 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -264,7 +264,7 @@ let implicits_of_glob_constr ?(with_products=true) l =
             let () = match bk with
             | Implicit ->
 	       Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ 
-			      pr_name na ++ strbrk " and following binders")
+			      Name.print na ++ strbrk " and following binders")
             | _ -> ()
             in []
       | GLambda (na, bk, t, b) -> abs na bk b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 04b7f7f3f1..8e876ec16d 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -159,7 +159,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
 	  e',Some (Loc.tag ?loc (ind,nal')) in
 	let e',na' = g e' na in
 	(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
-      let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
+      let fold (idl,e) na = let (e,na) = g e na in ((Name.cons na idl,e),na) in
       let eqnl' = List.map (fun (patl,rhs) ->
 	let ((idl,e),patl) =
 	  List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a79f10df6b..94bbc60eaf 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -83,13 +83,13 @@ let ids_of_cases_tomatch tms =
     (fun (_, ona, indnal) l ->
       Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
       indnal
-        (Option.fold_right (down_located (name_fold Id.Set.add)) ona l))
+        (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l))
     tms Id.Set.empty
 
 let rec fold_constr_expr_binders g f n acc b = function
   | (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
-      let n' = List.fold_right (name_fold g) nal n in
+      let n' = List.fold_right (Name.fold_right g) nal n in
       f n (fold_constr_expr_binders g f n' acc b l) t
   | [] ->
       f n acc b
@@ -97,10 +97,10 @@ let rec fold_constr_expr_binders g f n acc b = function
 let rec fold_local_binders g f n acc b = function
   | CLocalAssum (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
-      let n' = List.fold_right (name_fold g) nal n in
+      let n' = List.fold_right (Name.fold_right g) nal n in
       f n (fold_local_binders g f n' acc b l) t
   | CLocalDef ((_,na),c,t)::l ->
-      Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t
+      Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
   | CLocalPattern (_,(pat,t))::l ->
       let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
       Option.fold_left (f n) acc t
@@ -112,7 +112,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
   | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
   | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
   | CLetIn (na,a,t,b) ->
-     f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
+     f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
   | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
   | CCast (a,CastCoerce) -> f n acc a
   | CNotation (_,(l,ll,bll)) ->
@@ -133,12 +133,12 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
 	let ids = ids_of_pattern_list patl in
 	f (Id.Set.fold g ids n) acc rhs) bl acc
   | CLetTuple (nal,(ona,po),b,c) ->
-      let n' = List.fold_right (down_located (name_fold g)) nal n in
-      f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c
+      let n' = List.fold_right (down_located (Name.fold_right g)) nal n in
+      f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c
   | CIf (c,(ona,po),b1,b2) ->
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left
-	(f (Option.fold_right (down_located (name_fold g)) ona n)) acc po
+	(f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po
   | CFix (_,l) ->
       let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
       List.fold_right (fun (_,(_,o),lb,t,c) acc ->
@@ -198,7 +198,7 @@ let split_at_annot bl na =
 
 (* Used in correctness and interface *)
 
-let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e
+let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e
 
 let map_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
@@ -212,7 +212,7 @@ let map_local_binders f g e bl =
       CLocalAssum(nal,k,ty) ->
         (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
     | CLocalDef((loc,na),c,ty) ->
-        (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
+        (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
     | CLocalPattern (loc,(pat,t)) ->
         let ids = ids_of_pattern pat in
         (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in
@@ -228,7 +228,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function
   | CLambdaN (bl,b) ->
       let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b)
   | CLetIn (na,a,t,b) ->
-      CLetIn (na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b)
+      CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b)
   | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
   | CNotation (n,(l,ll,bll)) ->
       (* This is an approximation because we don't know what binds what *)
@@ -247,11 +247,11 @@ let map_constr_expr_with_binders g f e = CAst.map (function
       let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
       CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
   | CLetTuple (nal,(ona,po),b,c) ->
-      let e' = List.fold_right (down_located (name_fold g)) nal e in
-      let e'' = Option.fold_right (down_located (name_fold g)) ona e in
+      let e' = List.fold_right (down_located (Name.fold_right g)) nal e in
+      let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in
       CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
   | CIf (c,(ona,po),b1,b2) ->
-      let e' = Option.fold_right (down_located (name_fold g)) ona e in
+      let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in
       CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
   | CFix (id,dl) ->
       CFix (id,List.map (fun (id,n,bl,t,d) ->