diff options
34 files changed, 255 insertions, 152 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 7fad65bf0..3f3b0a870 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -51,6 +51,12 @@ In Constrexpr_ops: interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type. +In Nameops: + + The API has been made more uniform. New combinators added in the + "Name" space name. Function "out_name" now fails with IsAnonymous + rather than with Failure "Nameops.out_name". + Location handling and AST attributes: Location handling has been reworked. First, Loc.ghost has been diff --git a/engine/termops.ml b/engine/termops.ml index ca32c06a7..1af9bd1ff 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -31,10 +31,6 @@ let pr_sort_family = function | InProp -> (str "Prop") | InType -> (str "Type") -let pr_name = function - | Name id -> pr_id id - | Anonymous -> str "_" - let pr_con sp = str(string_of_con sp) let pr_fix pr_constr ((t,i),(lna,tl,bl)) = @@ -42,7 +38,7 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) = hov 1 (str"fix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,i,ty,bd) -> - pr_name na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ + Name.print na ++ str"/" ++ int i ++ str":" ++ pr_constr ty ++ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") @@ -65,10 +61,10 @@ let rec pr_constr c = match kind_of_term c with (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ pr_constr c ++ str")") | Lambda (na,t,c) -> hov 1 - (str"fun " ++ pr_name na ++ str":" ++ + (str"fun " ++ Name.print na ++ str":" ++ pr_constr t ++ str" =>" ++ spc() ++ pr_constr c) | LetIn (na,b,t,c) -> hov 0 - (str"let " ++ pr_name na ++ str":=" ++ pr_constr b ++ + (str"let " ++ Name.print na ++ str":=" ++ pr_constr b ++ str":" ++ brk(1,2) ++ pr_constr t ++ cut() ++ pr_constr c) | App (c,l) -> hov 1 @@ -93,7 +89,7 @@ let rec pr_constr c = match kind_of_term c with hov 1 (str"cofix " ++ int i ++ spc() ++ str"{" ++ v 0 (prlist_with_sep spc (fun (na,ty,bd) -> - pr_name na ++ str":" ++ pr_constr ty ++ + Name.print na ++ str":" ++ pr_constr ty ++ cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") @@ -308,8 +304,8 @@ let pr_evar_universe_context ctx = let print_env_short env = let print_constr = print_kconstr in let pr_rel_decl = function - | RelDecl.LocalAssum (n,_) -> pr_name n - | RelDecl.LocalDef (n,b,_) -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" + | RelDecl.LocalAssum (n,_) -> Name.print n + | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")" in let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in let nc = List.rev (named_context env) in diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4c29fc809..f6da10c96 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 1d5d8e865..b8d333f0d 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 diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index cfc6e6c2a..ade524141 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 6f9100911..ec8fa498c 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -184,7 +184,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 a79f10df6..94bbc60ea 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) -> diff --git a/kernel/names.ml b/kernel/names.ml index afdbe0c0d..ae3403335 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -104,8 +104,12 @@ struct | _ -> false let hash = function - | Anonymous -> 0 - | Name id -> Id.hash id + | Anonymous -> 0 + | Name id -> Id.hash id + + let print = function + | Anonymous -> str "_" + | Name id -> Id.print id module Self_Hashcons = struct diff --git a/kernel/names.mli b/kernel/names.mli index 5b0163aa5..c73eb197b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -105,6 +105,9 @@ sig val hcons : t -> t (** Hashconsing over names. *) + val print : t -> Pp.std_ppcmds + (** Pretty-printer (print "_" for [Anonymous]. *) + end (** {6 Type aliases} *) diff --git a/library/nameops.ml b/library/nameops.ml index 098f5112f..b73bd7eb3 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -14,10 +14,6 @@ open Names let pr_id id = Id.print id -let pr_name = function - | Anonymous -> str "_" - | Name id -> pr_id id - (* Utilities *) let code_of_0 = Char.code '0' @@ -124,34 +120,82 @@ let atompart_of_id id = fst (repr_ident id) (* Names *) -let out_name = function - | Name id -> id - | Anonymous -> failwith "Nameops.out_name" +module type ExtName = +sig + + include module type of struct include Names.Name end + + exception IsAnonymous + + val fold_left : ('a -> Id.t -> 'a) -> 'a -> t -> 'a + val fold_right : (Id.t -> 'a -> 'a) -> t -> 'a -> 'a + val iter : (Id.t -> unit) -> t -> unit + val map : (Id.t -> Id.t) -> t -> t + val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> t -> 'a * t + val get_id : t -> Id.t + val pick : t -> t -> t + val cons : t -> Id.t list -> Id.t list + val to_option : Name.t -> Id.t option + +end + +module Name : ExtName = +struct + + include Names.Name + + exception IsAnonymous + + let fold_left f a = function + | Name id -> f a id + | Anonymous -> a + + let fold_right f na a = + match na with + | Name id -> f id a + | Anonymous -> a + + let iter f na = fold_right (fun x () -> f x) na () + + let map f = function + | Name id -> Name (f id) + | Anonymous -> Anonymous + + let fold_map f a = function + | Name id -> let (a, id) = f a id in (a, Name id) + | Anonymous -> a, Anonymous + + let get_id = function + | Name id -> id + | Anonymous -> raise IsAnonymous -let name_fold f na a = - match na with - | Name id -> f id a - | Anonymous -> a + let pick na1 na2 = + match na1 with + | Name _ -> na1 + | Anonymous -> na2 -let name_iter f na = name_fold (fun x () -> f x) na () + let cons na l = + match na with + | Anonymous -> l + | Name id -> id::l -let name_cons na l = - match na with - | Anonymous -> l - | Name id -> id::l + let to_option = function + | Anonymous -> None + | Name id -> Some id -let name_app f = function - | Name id -> Name (f id) - | Anonymous -> Anonymous +end -let name_fold_map f e = function - | Name id -> let (e,id) = f e id in (e,Name id) - | Anonymous -> e,Anonymous +open Name -let name_max na1 na2 = - match na1 with - | Name _ -> na1 - | Anonymous -> na2 +(* Compatibility *) +let out_name = get_id +let name_fold = fold_right +let name_iter = iter +let name_app = map +let name_fold_map = fold_map +let name_cons = cons +let name_max = pick +let pr_name = print let pr_lab l = Label.print l diff --git a/library/nameops.mli b/library/nameops.mli index 3a67b61a1..abfc09db8 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -9,8 +9,6 @@ open Names (** Identifiers and names *) -val pr_id : Id.t -> Pp.std_ppcmds -val pr_name : Name.t -> Pp.std_ppcmds val make_ident : string -> int option -> Id.t val repr_ident : Id.t -> string * int option @@ -50,16 +48,69 @@ val increment_subscript : Id.t -> Id.t val forget_subscript : Id.t -> Id.t +module Name : sig + + include module type of struct include Names.Name end + + exception IsAnonymous + + val fold_left : ('a -> Id.t -> 'a) -> 'a -> Name.t -> 'a + (** [fold_left f na a] is [f id a] if [na] is [Name id], and [a] otherwise. *) + + val fold_right : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a + (** [fold_right f a na] is [f a id] if [na] is [Name id], and [a] otherwise. *) + + val iter : (Id.t -> unit) -> Name.t -> unit + (** [iter f na] does [f id] if [na] equals [Name id], nothing otherwise. *) + + val map : (Id.t -> Id.t) -> Name.t -> t + (** [map f na] is [Anonymous] if [na] is [Anonymous] and [Name (f id)] if [na] is [Name id]. *) + + val fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t + (** [fold_map f na a] is [a',Name id'] when [na] is [Name id] and [f a id] is [(a',id')]. + It is [a,Anonymous] otherwise. *) + + val get_id : Name.t -> Id.t + (** [get_id] associates [id] to [Name id]. @raise IsAnonymous otherwise. *) + + val pick : Name.t -> Name.t -> Name.t + (** [pick na na'] returns [Anonymous] if both names are [Anonymous]. + Pick one of [na] or [na'] otherwise. *) + + val cons : Name.t -> Id.t list -> Id.t list + (** [cons na l] returns [id::l] if [na] is [Name id] and [l] otherwise. *) + + val to_option : Name.t -> Id.t option + (** [to_option Anonymous] is [None] and [to_option (Name id)] is [Some id] *) + +end + val out_name : Name.t -> Id.t -(** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"] - otherwise. *) +(** @deprecated Same as [Name.get_id] *) val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a +(** @deprecated Same as [Name.fold_right] *) + val name_iter : (Id.t -> unit) -> Name.t -> unit -val name_cons : Name.t -> Id.t list -> Id.t list +(** @deprecated Same as [Name.iter] *) + val name_app : (Id.t -> Id.t) -> Name.t -> Name.t +(** @deprecated Same as [Name.map] *) + val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t +(** @deprecated Same as [Name.fold_map] *) + val name_max : Name.t -> Name.t -> Name.t +(** @deprecated Same as [Name.pick] *) + +val name_cons : Name.t -> Id.t list -> Id.t list +(** @deprecated Same as [Name.cons] *) + +val pr_name : Name.t -> Pp.std_ppcmds +(** @deprecated Same as [Name.print] *) + +val pr_id : Id.t -> Pp.std_ppcmds +(** @deprecated Same as [Names.Id.print] *) val pr_lab : Label.t -> Pp.std_ppcmds diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 434fb14a6..0041797de 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -944,7 +944,7 @@ let generalize_non_dep hyp g = ((* observe_tac "thin" *) (thin to_revert)) g -let id_of_decl = RelDecl.get_name %> Nameops.out_name +let id_of_decl = RelDecl.get_name %> Nameops.Name.get_id let var_of_decl = id_of_decl %> mkVar let revert idl = tclTHEN @@ -1127,11 +1127,11 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ) in observe (str "full_params := " ++ - prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id) + prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) full_params ); observe (str "princ_params := " ++ - prlist_with_sep spc (RelDecl.get_name %> Nameops.out_name %> Ppconstr.pr_id) + prlist_with_sep spc (RelDecl.get_name %> Nameops.Name.get_id %> Ppconstr.pr_id) princ_params ); observe (str "fbody_with_full_params := " ++ @@ -1158,7 +1158,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (fun i types -> let types = prod_applist (project g) types (List.rev_map var_of_decl princ_params) in { idx = idxs.(i) - fix_offset; - name = Nameops.out_name (fresh_id names.(i)); + name = Nameops.Name.get_id (fresh_id names.(i)); types = types; offset = fix_offset; nb_realargs = @@ -1181,7 +1181,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let first_args = Array.init nargs (fun i -> mkRel (nargs -i)) in let app_f = mkApp(f,first_args) in let pte_args = (Array.to_list first_args)@[app_f] in - let app_pte = applist(mkVar (Nameops.out_name pte),pte_args) in + let app_pte = applist(mkVar (Nameops.Name.get_id pte),pte_args) in let body_with_param,num = let body = get_body fnames.(i) in let body_with_full_params = @@ -1208,9 +1208,9 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam num_in_block = num } in -(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++ *) +(* observe (str "binding " ++ Ppconstr.pr_id (Nameops.Name.get_id pte) ++ *) (* str " to " ++ Ppconstr.pr_id info.name); *) - (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info) + (Id.Map.add (Nameops.Name.get_id pte) info acc_map,info::acc_info) ) 0 (Id.Map.empty,[]) @@ -1284,7 +1284,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam (do_replace evd full_params (fix_info.idx + List.length princ_params) - (args_id@(List.map (RelDecl.get_name %> Nameops.out_name) princ_params)) + (args_id@(List.map (RelDecl.get_name %> Nameops.Name.get_id) princ_params)) (all_funs.(fix_info.num_in_block)) fix_info.num_in_block all_funs @@ -1563,17 +1563,17 @@ let prove_principle_for_gen | _ -> assert false in (* observe (str "rec_arg_id := " ++ pr_lconstr (mkVar rec_arg_id)); *) - let subst_constrs = List.map (get_name %> Nameops.out_name %> mkVar) (pre_rec_arg@princ_info.params) in + let subst_constrs = List.map (get_name %> Nameops.Name.get_id %> mkVar) (pre_rec_arg@princ_info.params) in let relation = substl subst_constrs relation in let input_type = substl subst_constrs rec_arg_type in - let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in + let wf_thm_id = Nameops.Name.get_id (fresh_id (Name (Id.of_string "wf_R"))) in let acc_rec_arg_id = - Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) + Nameops.Name.get_id (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id))))) in let revert l = tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l)) in - let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in + let fix_id = Nameops.Name.get_id (fresh_id (Name hrec_id)) in let prove_rec_arg_acc g = ((* observe_tac "prove_rec_arg_acc" *) (tclCOMPLETE @@ -1591,7 +1591,7 @@ let prove_principle_for_gen ) g in - let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in + let args_ids = List.map (get_name %> Nameops.Name.get_id) princ_info.args in let lemma = match !tcc_lemma_ref with | Undefined -> user_err Pp.(str "No tcc proof !!") @@ -1639,7 +1639,7 @@ let prove_principle_for_gen [ observe_tac "start_tac" start_tac; h_intros - (List.rev_map (get_name %> Nameops.out_name) + (List.rev_map (get_name %> Nameops.Name.get_id) (princ_info.args@princ_info.branches@princ_info.predicates@princ_info.params) ); (* observe_tac "" *) Proofview.V82.of_tactic (assert_by @@ -1677,14 +1677,14 @@ let prove_principle_for_gen in let acc_inv = lazy (mkApp(Lazy.force acc_inv, [|mkVar acc_rec_arg_id|])) in let predicates_names = - List.map (get_name %> Nameops.out_name) princ_info.predicates + List.map (get_name %> Nameops.Name.get_id) princ_info.predicates in let pte_info = { proving_tac = (fun eqs -> (* msgnl (str "tcc_list := "++ prlist_with_sep spc Ppconstr.pr_id !tcc_list); *) -(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.args)); *) -(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.out_name na)) princ_info.params)); *) +(* msgnl (str "princ_info.args := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.args)); *) +(* msgnl (str "princ_info.params := "++ prlist_with_sep spc Ppconstr.pr_id (List.map (fun (na,_,_) -> (Nameops.Name.get_id na)) princ_info.params)); *) (* msgnl (str "acc_rec_arg_id := "++ Ppconstr.pr_id acc_rec_arg_id); *) (* msgnl (str "eqs := "++ prlist_with_sep spc Ppconstr.pr_id eqs); *) @@ -1693,7 +1693,7 @@ let prove_principle_for_gen is_mes acc_inv fix_id (!tcc_list@(List.map - (get_name %> Nameops.out_name) + (get_name %> Nameops.Name.get_id) (princ_info.args@princ_info.params) )@ ([acc_rec_arg_id])) eqs ) @@ -1722,7 +1722,7 @@ let prove_principle_for_gen (* observe_tac "instanciate_hyps_with_args" *) (instanciate_hyps_with_args make_proof - (List.map (get_name %> Nameops.out_name) princ_info.branches) + (List.map (get_name %> Nameops.Name.get_id) princ_info.branches) (List.rev args_ids) ) gl' diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 18d63dd94..942527167 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -62,7 +62,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = then List.tl args else args in - Context.Named.Declaration.LocalAssum (Nameops.out_name (Context.Rel.Declaration.get_name decl), + Context.Named.Declaration.LocalAssum (Nameops.Name.get_id (Context.Rel.Declaration.get_name decl), Term.compose_prod real_args (mkSort new_sort)) in let new_predicates = @@ -185,11 +185,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = with | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end @@ -214,11 +214,11 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = with | Toberemoved -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [dummy_var] 1 b) in new_b, List.map pop binders_to_remove_from_b | Toberemoved_with_rel (n,c) -> -(* observe (str "Decl of "++Ppconstr.pr_name x ++ str " is removed "); *) +(* observe (str "Decl of "++Ppconstr.Name.print x ++ str " is removed "); *) let new_b,binders_to_remove_from_b = compute_new_princ_type remove env (substnl [c] n b) in new_b, list_add_set_eq eq_constr (mkRel n) (List.map pop binders_to_remove_from_b) end diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 74c0eb4cc..4946285e1 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -200,13 +200,13 @@ let is_rec names = | GIf(b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) | GProd(na,_,t,b) | GLambda(na,_,t,b) -> - lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b + lookup names t || lookup (Nameops.Name.fold_right Id.Set.remove na names) b | GLetIn(na,b,t,c) -> - lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.Name.fold_right Id.Set.remove na names) c | GLetTuple(nal,_,t,b) -> lookup names t || lookup (List.fold_left - (fun acc na -> Nameops.name_fold Id.Set.remove na acc) + (fun acc na -> Nameops.Name.fold_right Id.Set.remove na acc) names nal ) @@ -885,7 +885,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun (loc,n) -> CAst.make ?loc @@ - CRef(Libnames.Ident(loc, Nameops.out_name n),None)) + CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None)) nal | Constrexpr.CLocalPattern _ -> assert false ) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index d68bdc215..12232dd83 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -421,7 +421,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let params_bindings,avoid = List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -431,7 +431,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 2f9f70876..62eba9513 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -879,7 +879,7 @@ let rec make_rewrite_list expr_info max = function let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in let def_na,_,_ = destProd sigma t in - Nameops.out_name k_na,Nameops.out_name def_na + Nameops.Name.get_id k_na,Nameops.Name.get_id def_na in Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences true (* dep proofs also: *) true @@ -905,7 +905,7 @@ let make_rewrite expr_info l hp max = let k_na,_,t = destProd sigma t_eq in let _,_,t = destProd sigma t in let def_na,_,_ = destProd sigma t in - Nameops.out_name k_na,Nameops.out_name def_na + Nameops.Name.get_id k_na,Nameops.Name.get_id def_na in observe_tac (str "general_rewrite_bindings") (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index a001c6a2b..67d2b452a 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -571,7 +571,7 @@ type 'a extra_genarg_printer = str "=>" ++ brk (1,4) ++ pr t)) | All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t - let pr_funvar n = spc () ++ pr_name n + let pr_funvar n = spc () ++ Name.print n let pr_let_clause k pr (id,(bl,t)) = hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 75f89a81e..f44ccbd3b 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -502,7 +502,7 @@ let print_ltacs () = | Tacexpr.TacFun (l, t) -> (l, t) | _ -> ([], body) in - let pr_ltac_fun_arg n = spc () ++ pr_name n in + let pr_ltac_fun_arg n = spc () ++ Name.print n in hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) in Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index e431a13bc..82711dd46 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -718,7 +718,7 @@ let split_ltac_fun = function | TacFun (l,t) -> (l,t) | t -> ([],t) -let pr_ltac_fun_arg n = spc () ++ pr_name n +let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac id = try diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index a9ec779d1..31c1b79ee 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1116,11 +1116,11 @@ let cons_and_check_name id l = let rec read_match_goal_hyps lfun ist env sigma lidh = function | (Hyp ((loc,na) as locna,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Hyp (locna,read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | (Def ((loc,na) as locna,mv,mp))::tl -> - let lidh' = name_fold cons_and_check_name na lidh in + let lidh' = Name.fold_right cons_and_check_name na lidh in Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) | [] -> [] @@ -1423,7 +1423,7 @@ and tactic_of_value ist vle = (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++ Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++ Pp.str (String.plural numargs "variable") ++ Pp.str " " ++ - pr_enum pr_name vars ++ Pp.str ".") + pr_enum Name.print vars ++ Pp.str ".") | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.") else if has_type vle (topwit wit_tactic) then let tac = out_gen (topwit wit_tactic) vle in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c2c8065a9..f16f393f6 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 752819aa3..6f099c8df 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 bf62cea6b..630f80ad2 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 923d7d938..faf44099c 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -215,20 +215,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 @@ -242,7 +242,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 @@ -371,12 +371,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 1c8ad0cdd..0818a5525 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 diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index f76555b04..60511d913 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 diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index c328b6032..6aa136b60 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -56,7 +56,7 @@ open Decl_kinds 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_smart_global = Pputils.pr_or_by_notation pr_reference @@ -1022,13 +1022,13 @@ open Decl_kinds | n, { name = id; recarg_like = k; notation_scope = s; implicit_status = imp } :: tl -> - spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++ + spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++ print_arguments (Option.map pred n) tl in let rec print_implicits = function | [] -> mt () | (name, impl) :: rest -> - spc() ++ pr_br impl (pr_name name) ++ print_implicits rest + spc() ++ pr_br impl (Name.print name) ++ print_implicits rest in print_arguments nargs args ++ if not (List.is_empty more_implicits) then diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 0f7da3613..2b21b3f9e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -132,7 +132,7 @@ let print_impargs_list prefix l = let print_renames_list prefix l = if List.is_empty l then [] else [add_colon prefix ++ str "Arguments are renamed to " ++ - hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map pr_name l))] + hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))] let need_expansion impl ref = let typ = Global.type_of_global_unsafe ref in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 33a86402e..87b31849e 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -433,7 +433,7 @@ let explain_no_such_bound_variable evd id = | Cltyp (na, _) -> na | Clval (na, _, _) -> na in - if na != Anonymous then out_name na :: l else l + if na != Anonymous then Name.get_id na :: l else l in let mvl = List.fold_left fold [] (Evd.meta_list evd) in user_err ~hdr:"Evd.meta_with_name" diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7e8cb4e63..85971e665 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2975,7 +2975,7 @@ let specialize (c,lbind) ipat = if occur_meta clause.evd term then user_err (str "Cannot infer an instance for " ++ - pr_name (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++ + Name.print (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++ str "."); clause.evd, term in let typ = Retyping.get_type_of env sigma term in diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index cf534f13a..b99ccbf4a 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -533,7 +533,7 @@ open Namegen let compute_bl_goal ind lnamesparrec nparrec = let eqI, eff = eqI ind lnamesparrec in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in @@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in - let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in let eqI, eff = eqI ind lnamesparrec in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and @@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec = check_not_is_defined (); let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in diff --git a/vernac/command.ml b/vernac/command.ml index e2ebb4d7f..6ece585a9 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -411,8 +411,8 @@ let mk_mltype_data evdref env assums arity indname = (is_ml_type,indname,assums) let prepare_param = function - | LocalAssum (na,t) -> out_name na, LocalAssumEntry t - | LocalDef (na,b,_) -> out_name na, LocalDefEntry b + | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t + | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. @@ -590,7 +590,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter is_local_assum ctx_params in - let params = List.map (RelDecl.get_name %> out_name) assums in + let params = List.map (RelDecl.get_name %> Name.get_id) assums in (* Interpret the arities *) let arities = List.map (interp_ind_arity env_params evdref) indl in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 17bb87f2a..6d8dd82ac 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -682,12 +682,12 @@ let explain_wrong_abstraction_type env sigma na abs expected result = let explain_abstraction_over_meta _ m n = strbrk "Too complex unification problem: cannot find a solution for both " ++ - pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "." + Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "." let explain_non_linear_unification env sigma m t = let t = EConstr.to_constr sigma t in strbrk "Cannot unambiguously instantiate " ++ - pr_name m ++ str ":" ++ + Name.print m ++ str ":" ++ strbrk " which would require to abstract twice on " ++ pr_lconstr_env env sigma t ++ str "." @@ -1055,7 +1055,7 @@ let explain_refiner_bad_type arg ty conclty = let explain_refiner_unresolved_bindings l = str "Unable to find an instance for the " ++ str (String.plural (List.length l) "variable") ++ spc () ++ - prlist_with_sep pr_comma pr_name l ++ str"." + prlist_with_sep pr_comma Name.print l ++ str"." let explain_refiner_cannot_apply t harg = str "In refiner, a term of type" ++ brk(1,1) ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6c1d64cfe..405d37927 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1003,12 +1003,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags let err_extra_args names = user_err ~hdr:"vernac_declare_arguments" (strbrk "Extra arguments: " ++ - prlist_with_sep pr_comma pr_name names ++ str ".") + prlist_with_sep pr_comma Name.print names ++ str ".") in let err_missing_args names = user_err ~hdr:"vernac_declare_arguments" (strbrk "The following arguments are not declared: " ++ - prlist_with_sep pr_comma pr_name names ++ str ".") + prlist_with_sep pr_comma Name.print names ++ str ".") in let rec check_extra_args extra_args = @@ -1093,14 +1093,14 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags match !example_renaming with | None -> mt () | Some (o,n) -> - str "Argument " ++ pr_name o ++ - str " renamed to " ++ pr_name n ++ str "."); + str "Argument " ++ Name.print o ++ + str " renamed to " ++ Name.print n ++ str "."); let duplicate_names = List.duplicates Name.equal (List.filter ((!=) Anonymous) names) in if not (List.is_empty duplicate_names) then begin - let duplicates = prlist_with_sep pr_comma pr_name duplicate_names in + let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in user_err (strbrk "Some argument names are duplicated: " ++ duplicates) end; @@ -1129,7 +1129,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags anonymous argument implicit *) | Anonymous :: _, (name, _) :: _ -> user_err ~hdr:"vernac_declare_arguments" - (strbrk"Argument "++ pr_name name ++ + (strbrk"Argument "++ Name.print name ++ strbrk " cannot be declared implicit.") | Name id :: inf_names, (name, impl) :: implicits -> |