From f2ab2825077bf8344d2e55be433efb1891212589 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 May 2018 13:34:22 +0200 Subject: Collecting Array.smart_* functions into a module Array.Smart. --- proofs/logic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/logic.ml b/proofs/logic.ml index 4934afa83..218b2671e 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -481,7 +481,7 @@ and mk_arggoals sigma goal goalacc funty allargs = let env = Goal.V82.env sigma goal in raise (RefinerError (env,sigma,CannotApply (t, harg))) in - Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs + Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in -- cgit v1.2.3 From 33b5074f24270c202a9922f21d445c12cc6b3b3d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 23 May 2018 13:34:46 +0200 Subject: Collecting List.smart_* functions into a module List.Smart. --- checker/declarations.ml | 2 +- checker/term.ml | 2 +- checker/univ.ml | 6 +++--- clib/cList.ml | 48 +++++++++++++++++++++++++++++--------------- clib/cList.mli | 17 ++++++++++++---- interp/impargs.ml | 2 +- interp/notation.ml | 2 +- interp/notation_ops.ml | 12 +++++------ kernel/context.ml | 4 ++-- kernel/declareops.ml | 8 ++++---- kernel/modops.ml | 4 ++-- kernel/univ.ml | 10 ++++----- library/lib.ml | 2 +- plugins/extraction/mlutil.ml | 6 +++--- pretyping/detyping.ml | 12 +++++------ pretyping/glob_ops.ml | 10 ++++----- pretyping/patternops.ml | 4 ++-- pretyping/pretyping.ml | 2 +- pretyping/recordops.ml | 2 +- pretyping/typeclasses.ml | 10 ++++----- proofs/redexpr.ml | 4 ++-- tactics/hints.ml | 12 +++++------ 22 files changed, 103 insertions(+), 78 deletions(-) (limited to 'proofs') diff --git a/checker/declarations.ml b/checker/declarations.ml index ca31e143f..3368d68f7 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -513,7 +513,7 @@ let subst_decl_arity f g sub ar = let subst_rel_declaration sub = Term.map_rel_decl (subst_mps sub) -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) +let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub) let constant_is_polymorphic cb = match cb.const_universes with diff --git a/checker/term.ml b/checker/term.ml index 0236f7867..509634bdb 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -243,7 +243,7 @@ let map_rel_decl f = function LocalDef (n, body', typ') let map_rel_context f = - List.smartmap (map_rel_decl f) + List.Smart.map (map_rel_decl f) let extended_rel_list n hyps = let rec reln l p = function diff --git a/checker/univ.ml b/checker/univ.ml index d3eab8613..15673736f 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -314,7 +314,7 @@ struct let for_all = List.for_all - let smartmap = List.smartmap + let smart_map = List.Smart.map end @@ -956,7 +956,7 @@ let subst_instance_instance s i = let subst_instance_universe s u = let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' @@ -1097,7 +1097,7 @@ let subst_univs_level_level subst l = let subst_univs_level_universe subst u = let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' diff --git a/clib/cList.ml b/clib/cList.ml index 8727f4696..7621793d4 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -39,6 +39,7 @@ sig val map_filter_i : (int -> 'a -> 'b option) -> 'a list -> 'b list val filter_with : bool list -> 'a list -> 'a list val smartmap : ('a -> 'a) -> 'a list -> 'a list + [@@ocaml.deprecated "Same as [Smart.map]"] val map_left : ('a -> 'b) -> 'a list -> 'b list val map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list val map2_i : @@ -53,6 +54,7 @@ sig (int -> 'a -> bool) -> 'a list -> 'a list * 'a list val map_of_array : ('a -> 'b) -> 'a array -> 'b list val smartfilter : ('a -> bool) -> 'a list -> 'a list + [@@ocaml.deprecated "Same as [Smart.map]"] val extend : bool list -> 'a -> 'a list -> 'a list val count : ('a -> bool) -> 'a list -> int val index : 'a eq -> 'a -> 'a list -> int @@ -117,6 +119,12 @@ sig ('a -> 'b -> 'b option) -> 'b -> 'a list list -> 'b list val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list + module Smart : + sig + val map : ('a -> 'a) -> 'a list -> 'a list + val filter : ('a -> bool) -> 'a list -> 'a list + end + module type MonoS = sig type elt val equal : elt list -> elt list -> bool @@ -365,13 +373,6 @@ let assign l n e = in assrec [] l n -let rec smartmap f l = match l with - [] -> l - | h::tl -> - let h' = f h and tl' = smartmap f tl in - if h'==h && tl'==tl then l - else h'::tl' - let map_left = map let map2_i f i l1 l2 = @@ -398,15 +399,6 @@ let map4 f l1 l2 l3 l4 = in map (l1,l2,l3,l4) -let rec smartfilter f l = match l with - [] -> l - | h::tl -> - let tl' = smartfilter f tl in - if f h then - if tl' == tl then l - else h :: tl' - else tl' - let rec extend l a l' = match l,l' with | true::l, b::l' -> b :: extend l a l' | false::l, l' -> a :: extend l a l' @@ -896,6 +888,30 @@ let rec factorize_left cmp = function (a,(b::List.map snd al)) :: factorize_left cmp l' | [] -> [] +module Smart = +struct + + let rec map f l = match l with + [] -> l + | h::tl -> + let h' = f h and tl' = map f tl in + if h'==h && tl'==tl then l + else h'::tl' + + let rec filter f l = match l with + [] -> l + | h::tl -> + let tl' = filter f tl in + if f h then + if tl' == tl then l + else h :: tl' + else tl' + +end + +let smartmap = Smart.map +let smartfilter = Smart.filter + module type MonoS = sig type elt val equal : elt list -> elt list -> bool diff --git a/clib/cList.mli b/clib/cList.mli index fd6d6a158..b3c151098 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -75,8 +75,7 @@ sig [b] is [true]. Raise [Invalid_argument _] when sizes differ. *) val smartmap : ('a -> 'a) -> 'a list -> 'a list - (** [smartmap f [a1...an] = List.map f [a1...an]] but if for all i - [f ai == ai], then [smartmap f l == l] *) + [@@ocaml.deprecated "Same as [Smart.map]"] val map_left : ('a -> 'b) -> 'a list -> 'b list (** As [map] but ensures the left-to-right order of evaluation. *) @@ -97,8 +96,7 @@ sig (** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *) val smartfilter : ('a -> bool) -> 'a list -> 'a list - (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i - [f ai = true], then [smartfilter f l == l] *) + [@@ocaml.deprecated "Same as [Smart.filter]"] val extend : bool list -> 'a -> 'a list -> 'a list (** [extend l a [a1..an]] assumes that the number of [true] in [l] is [n]; @@ -258,6 +256,17 @@ sig val factorize_left : 'a eq -> ('a * 'b) list -> ('a * 'b list) list + module Smart : + sig + val map : ('a -> 'a) -> 'a list -> 'a list + (** [Smart.map f [a1...an] = List.map f [a1...an]] but if for all i + [f ai == ai], then [Smart.map f l == l] *) + + val filter : ('a -> bool) -> 'a list -> 'a list + (** [Smart.filter f [a1...an] = List.filter f [a1...an]] but if for all i + [f ai = true], then [Smart.filter f l == l] *) + end + module type MonoS = sig type elt val equal : elt list -> elt list -> bool diff --git a/interp/impargs.ml b/interp/impargs.ml index 7e4c4ef4f..2db67c299 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -538,7 +538,7 @@ let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (subst,(req,l)) = - (ImplLocal,List.smartmap (subst_implicits_decl subst) l) + (ImplLocal,List.Smart.map (subst_implicits_decl subst) l) let impls_of_context ctx = let map (decl, impl) = match impl with diff --git a/interp/notation.ml b/interp/notation.ml index e6df7b96c..192c477be 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -741,7 +741,7 @@ let subst_arguments_scope (subst,(req,r,n,scl,cls)) = match subst_scope_class subst cl with | Some cl' as ocl' when cl' != cl -> ocl' | _ -> ocl in - let cls' = List.smartmap subst_cl cls in + let cls' = List.Smart.map subst_cl cls in (ArgsScopeNoDischarge,r',n,scl,cls') let discharge_arguments_scope (_,(req,r,n,l,_)) = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index dc6a103e0..eeda607e6 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -521,7 +521,7 @@ let rec subst_pat subst pat = | PatVar _ -> pat | PatCstr (((kn,i),j),cpl,n) -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_pat subst) cpl in + and cpl' = List.Smart.map (subst_pat subst) cpl in if kn' == kn && cpl' == cpl then pat else DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n) @@ -536,7 +536,7 @@ let rec subst_notation_constr subst bound raw = | NApp (r,rl) -> let r' = subst_notation_constr subst bound r - and rl' = List.smartmap (subst_notation_constr subst bound) rl in + and rl' = List.Smart.map (subst_notation_constr subst bound) rl in if r' == r && rl' == rl then raw else NApp(r',rl') @@ -573,7 +573,7 @@ let rec subst_notation_constr subst bound raw = | NCases (sty,rtntypopt,rl,branches) -> let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt - and rl' = List.smartmap + and rl' = List.Smart.map (fun (a,(n,signopt) as x) -> let a' = subst_notation_constr subst bound a in let signopt' = Option.map (fun ((indkn,i),nal as z) -> @@ -581,9 +581,9 @@ let rec subst_notation_constr subst bound raw = if indkn == indkn' then z else ((indkn',i),nal)) signopt in if a' == a && signopt' == signopt then x else (a',(n,signopt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun (cpl,r as branch) -> - let cpl' = List.smartmap (subst_pat subst) cpl + let cpl' = List.Smart.map (subst_pat subst) cpl and r' = subst_notation_constr subst bound r in if cpl' == cpl && r' == r then branch else (cpl',r')) @@ -610,7 +610,7 @@ let rec subst_notation_constr subst bound raw = | NRec (fk,idl,dll,tl,bl) -> let dll' = - Array.Smart.map (List.smartmap (fun (na,oc,b as x) -> + Array.Smart.map (List.Smart.map (fun (na,oc,b as x) -> let oc' = Option.smartmap (subst_notation_constr subst bound) oc in let b' = subst_notation_constr subst bound b in if oc' == oc && b' == b then x else (na,oc',b'))) dll in diff --git a/kernel/context.ml b/kernel/context.ml index 4f3f649c1..5d4a10184 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -192,7 +192,7 @@ struct let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given rel-context. *) - let map f = List.smartmap (Declaration.map_constr f) + let map f = List.Smart.map (Declaration.map_constr f) (** Perform a given action on every declaration in a given rel-context. *) let iter f = List.iter (Declaration.iter_constr f) @@ -392,7 +392,7 @@ struct let equal eq l = List.equal (fun c -> Declaration.equal eq c) l (** Map all terms in a given named-context. *) - let map f = List.smartmap (Declaration.map_constr f) + let map f = List.Smart.map (Declaration.map_constr f) (** Perform a given action on every declaration in a given named-context. *) let iter f = List.iter (Declaration.iter_constr f) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 90a6eb6f7..f2f43144e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -42,7 +42,7 @@ let map_decl_arity f g = function let hcons_template_arity ar = { template_param_levels = ar.template_param_levels; - (* List.smartmap (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *) + (* List.Smart.map (Option.smartmap Univ.hcons_univ_level) ar.template_param_levels; *) template_level = Univ.hcons_univ ar.template_level } (** {6 Constants } *) @@ -70,7 +70,7 @@ let is_opaque cb = match cb.const_body with let subst_rel_declaration sub = RelDecl.map_constr (subst_mps sub) -let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) +let subst_rel_context sub = List.Smart.map (subst_rel_declaration sub) let subst_const_type sub arity = if is_empty_subst sub then arity @@ -117,7 +117,7 @@ let subst_const_body sub cb = let hcons_rel_decl = RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Constr.hcons %> RelDecl.map_type Constr.hcons -let hcons_rel_context l = List.smartmap hcons_rel_decl l +let hcons_rel_context l = List.Smart.map hcons_rel_decl l let hcons_const_def = function | Undef inl -> Undef inl @@ -331,7 +331,7 @@ and hcons_structure_body sb = let sfb' = hcons_structure_field_body sfb in if l == l' && sfb == sfb' then fb else (l', sfb') in - List.smartmap map sb + List.Smart.map map sb and hcons_module_signature ms = hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms diff --git a/kernel/modops.ml b/kernel/modops.ml index bbf160db2..daee0f187 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -197,7 +197,7 @@ let rec subst_structure sub do_delta sign = let mtb' = subst_modtype sub do_delta mtb in if mtb==mtb' then orig else (l,SFBmodtype mtb') in - List.smartmap subst_body sign + List.Smart.map subst_body sign and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = fun is_mod sub subst_impl do_delta mb -> @@ -595,7 +595,7 @@ and clean_field l field = match field with if mb==mb' then field else (lab,SFBmodule mb') |_ -> field -and clean_structure l = List.smartmap (clean_field l) +and clean_structure l = List.Smart.map (clean_field l) and clean_signature l = functor_smartmap (clean_module_type l) (clean_structure l) diff --git a/kernel/univ.ml b/kernel/univ.ml index 6bcffdd45..9782312ca 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -456,10 +456,10 @@ struct let super l = if is_small l then type1 else - List.smartmap (fun x -> Expr.successor x) l + List.Smart.map (fun x -> Expr.successor x) l let addn n l = - List.smartmap (fun x -> Expr.addn n x) l + List.Smart.map (fun x -> Expr.addn n x) l let rec merge_univs l1 l2 = match l1, l2 with @@ -500,7 +500,7 @@ struct let for_all = List.for_all - let smartmap = List.smartmap + let smart_map = List.Smart.map let map = List.map end @@ -894,7 +894,7 @@ let subst_instance_instance s i = let subst_instance_universe s u = let f x = Universe.Expr.map (fun u -> subst_instance_level s u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' @@ -1100,7 +1100,7 @@ let subst_univs_level_level subst l = let subst_univs_level_universe subst u = let f x = Universe.Expr.map (fun u -> subst_univs_level_level subst u) x in - let u' = Universe.smartmap f u in + let u' = Universe.smart_map f u in if u == u' then u else Universe.sort u' diff --git a/library/lib.ml b/library/lib.ml index 8a54995b9..128b27e75 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -51,7 +51,7 @@ let subst_objects subst seg = if obj' == obj then node else (id, obj') in - List.smartmap subst_one seg + List.Smart.map subst_one seg (*let load_and_subst_objects i prefix subst seg = List.rev (List.fold_left (fun seg (id,obj as node) -> diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index f508a8860..9f5c1f1a1 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -550,15 +550,15 @@ let dump_unused_vars a = if v' == v then a else MLfix (i,ids,v') | MLapp (b,l) -> - let b' = ren env b and l' = List.smartmap (ren env) l in + let b' = ren env b and l' = List.Smart.map (ren env) l in if b' == b && l' == l then a else MLapp (b',l') | MLcons(t,r,l) -> - let l' = List.smartmap (ren env) l in + let l' = List.Smart.map (ren env) l in if l' == l then a else MLcons (t,r,l') | MLtuple l -> - let l' = List.smartmap (ren env) l in + let l' = List.Smart.map (ren env) l in if l' == l then a else MLtuple l' | MLmagic b -> diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index ea2889dea..e306fd6b3 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -920,7 +920,7 @@ let rec subst_cases_pattern subst = DAst.map (function | PatVar _ as pat -> pat | PatCstr (((kn,i),j),cpl,n) as pat -> let kn' = subst_mind subst kn - and cpl' = List.smartmap (subst_cases_pattern subst) cpl in + and cpl' = List.Smart.map (subst_cases_pattern subst) cpl in if kn' == kn && cpl' == cpl then pat else PatCstr (((kn',i),j),cpl',n) ) @@ -940,7 +940,7 @@ let rec subst_glob_constr subst = DAst.map (function | GApp (r,rl) as raw -> let r' = subst_glob_constr subst r - and rl' = List.smartmap (subst_glob_constr subst) rl in + and rl' = List.Smart.map (subst_glob_constr subst) rl in if r' == r && rl' == rl then raw else GApp(r',rl') @@ -964,7 +964,7 @@ let rec subst_glob_constr subst = DAst.map (function | GCases (sty,rtno,rl,branches) as raw -> let open CAst in let rtno' = Option.smartmap (subst_glob_constr subst) rtno - and rl' = List.smartmap (fun (a,x as y) -> + and rl' = List.Smart.map (fun (a,x as y) -> let a' = subst_glob_constr subst a in let (n,topt) = x in let topt' = Option.smartmap @@ -972,10 +972,10 @@ let rec subst_glob_constr subst = DAst.map (function let sp' = subst_mind subst sp in if sp == sp' then t else CAst.(make ?loc ((sp',i),y))) topt in if a == a' && topt == topt' then y else (a',(n,topt'))) rl - and branches' = List.smartmap + and branches' = List.Smart.map (fun ({loc;v=(idl,cpl,r)} as branch) -> let cpl' = - List.smartmap (subst_cases_pattern subst) cpl + List.Smart.map (subst_cases_pattern subst) cpl and r' = subst_glob_constr subst r in if cpl' == cpl && r' == r then branch else CAst.(make ?loc (idl,cpl',r'))) @@ -1003,7 +1003,7 @@ let rec subst_glob_constr subst = DAst.map (function let ra1' = Array.Smart.map (subst_glob_constr subst) ra1 and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in let bl' = Array.Smart.map - (List.smartmap (fun (na,k,obd,ty as dcl) -> + (List.Smart.map (fun (na,k,obd,ty as dcl) -> let ty' = subst_glob_constr subst ty in let obd' = Option.smartmap (subst_glob_constr subst) obd in if ty'==ty && obd'==obd then dcl else (na,k,obd',ty'))) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 95f02dceb..102e89400 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -338,7 +338,7 @@ let bound_glob_vars = pattern-matching expressions are usually rather small. *) let map_inpattern_binders f ({loc;v=(id,nal)} as x) = - let r = CList.smartmap f nal in + let r = CList.Smart.map f nal in if r == nal then x else CAst.make ?loc (id,r) @@ -355,7 +355,7 @@ let rec map_case_pattern_binders f = DAst.map (function | PatCstr (c,ps,na) as x -> let rna = f na in let rps = - CList.smartmap (fun p -> map_case_pattern_binders f p) ps + CList.Smart.map (fun p -> map_case_pattern_binders f p) ps in if rna == na && rps == ps then x else PatCstr(c,rps,rna) @@ -366,13 +366,13 @@ let map_cases_branch_binders f ({CAst.loc;v=(il,cll,rhs)} as x) : cases_clause = It is intended to be a superset of the free variable of the right-hand side, if I understand correctly. But I'm not sure when or how they are used. *) - let r = List.smartmap (fun cl -> map_case_pattern_binders f cl) cll in + let r = List.Smart.map (fun cl -> map_case_pattern_binders f cl) cll in if r == cll then x else CAst.make ?loc (il,r,rhs) let map_pattern_binders f tomatch branches = - CList.smartmap (fun tm -> map_tomatch_binders f tm) tomatch, - CList.smartmap (fun br -> map_cases_branch_binders f br) branches + CList.Smart.map (fun tm -> map_tomatch_binders f tm) tomatch, + CList.Smart.map (fun br -> map_cases_branch_binders f br) branches (** /mapping of names in binders *) diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index bc7ed6137..b425dc0e2 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -297,7 +297,7 @@ let rec subst_pattern subst pat = if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> - let args' = List.smartmap (subst_pattern subst) args in + let args' = List.Smart.map (subst_pattern subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> @@ -334,7 +334,7 @@ let rec subst_pattern subst pat = let c' = subst_pattern subst c in if c' == c then br else (i,n,c') in - let branches' = List.smartmap subst_branch branches in + let branches' = List.Smart.map subst_branch branches in if cip' == cip && typ' == typ && c' == c && branches' == branches then pat else PCase(cip', typ', c', branches') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6bf852fcd..de72f9427 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -421,7 +421,7 @@ let ltac_interp_name_env k0 lvar env sigma = let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in let open Context.Rel.Declaration in - let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + let ctxt' = List.Smart.map (map_name (ltac_interp_name lvar)) ctxt in if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env else push_rel_context sigma ctxt' (pop_rel_context n env sigma) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 84aceeedd..334bfc895 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -69,7 +69,7 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) = let projs' = (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *) (* the first component of subst_con. *) - List.smartmap + List.Smart.map (Option.smartmap (fun kn -> fst (subst_con_kn subst kn))) projs in diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 11cc6c1f0..5ad9dc691 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -180,11 +180,11 @@ let subst_class (subst,cl) = let do_subst_con c = Mod_subst.subst_constant subst c and do_subst c = Mod_subst.subst_mps subst c and do_subst_gr gr = fst (subst_global subst gr) in - let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in + let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in let do_subst_context (grs,ctx) = - List.smartmap (Option.smartmap do_subst_gr) grs, + List.Smart.map (Option.smartmap do_subst_gr) grs, do_subst_ctx ctx in - let do_subst_projs projs = List.smartmap (fun (x, y, z) -> + let do_subst_projs projs = List.Smart.map (fun (x, y, z) -> (x, y, Option.smartmap do_subst_con z)) projs in { cl_univs = cl.cl_univs; cl_impl = do_subst_gr cl.cl_impl; @@ -223,7 +223,7 @@ let discharge_class (_,cl) = | Some (_, ((tc,_), _)) -> Some tc.cl_impl) ctx' in - List.smartmap (Option.smartmap Lib.discharge_global) grs + List.Smart.map (Option.smartmap Lib.discharge_global) grs @ newgrs in grs', discharge_rel_context subst 1 ctx @ ctx' in let cl_impl' = Lib.discharge_global cl.cl_impl in @@ -239,7 +239,7 @@ let discharge_class (_,cl) = cl_impl = cl_impl'; cl_context = context; cl_props = props; - cl_projs = List.smartmap discharge_proj cl.cl_projs; + cl_projs = List.Smart.map discharge_proj cl.cl_projs; cl_strict = cl.cl_strict; cl_unique = cl.cl_unique } diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 6fb411938..a75711bae 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -92,9 +92,9 @@ let cache_strategy (_,str) = let subst_strategy (subs,(local,obj)) = local, - List.smartmap + List.Smart.map (fun (k,ql as entry) -> - let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in + let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in if ql==ql' then entry else (k,ql')) obj diff --git a/tactics/hints.ml b/tactics/hints.ml index 39034a19b..4eaff3fb9 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -448,7 +448,7 @@ let subst_path_atom subst p = | PathAny -> p | PathHints grs -> let gr' gr = fst (subst_global subst gr) in - let grs' = List.smartmap gr' grs in + let grs' = List.Smart.map gr' grs in if grs' == grs then p else PathHints grs' let rec subst_hints_path subst hp = @@ -654,7 +654,7 @@ struct let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l - let remove_sdl p sdl = List.smartfilter p sdl + let remove_sdl p sdl = List.Smart.filter p sdl let remove_he st p se = let sl1' = remove_sdl p se.sentry_nopat in @@ -666,7 +666,7 @@ struct let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in - let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in + let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } let remove_one gr db = remove_list [gr] db @@ -1104,13 +1104,13 @@ let subst_autohint (subst, obj) = let action = match obj.hint_action with | CreateDB _ -> obj.hint_action | AddTransparency (grs, b) -> - let grs' = List.smartmap (subst_evaluable_reference subst) grs in + let grs' = List.Smart.map (subst_evaluable_reference subst) grs in if grs == grs' then obj.hint_action else AddTransparency (grs', b) | AddHints hintlist -> - let hintlist' = List.smartmap subst_hint hintlist in + let hintlist' = List.Smart.map subst_hint hintlist in if hintlist' == hintlist then obj.hint_action else AddHints hintlist' | RemoveHints grs -> - let grs' = List.smartmap (subst_global_reference subst) grs in + let grs' = List.Smart.map (subst_global_reference subst) grs in if grs == grs' then obj.hint_action else RemoveHints grs' | AddCut path -> let path' = subst_hints_path subst path in -- cgit v1.2.3