diff options
33 files changed, 118 insertions, 82 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 38527249c..4500d371c 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -180,7 +180,7 @@ let ref_value_cache info ref = let body = match ref with | RelKey n -> - let (s,l) = info.i_rels in lift n (List.assoc (s-n) l) + let (s,l) = info.i_rels in lift n (List.assoc_f Int.equal (s-n) l) | VarKey id -> raise Not_found | ConstKey cst -> constant_value info.i_env cst in diff --git a/checker/inductive.ml b/checker/inductive.ml index 2dd76c4d3..e2c7f30ab 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -125,7 +125,9 @@ let sort_as_univ = function | Prop Pos -> type0_univ let cons_subst u su subst = - try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst + try + (u, sup su (List.assoc_f Universe.equal u subst)) :: + List.remove_assoc_f Universe.equal u subst with Not_found -> (u, su) :: subst let actualize_decl_level env lev t = diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 4b4b36865..734b330e7 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -219,8 +219,9 @@ let combine_params avoid fn applied needed = match app, need with [], [] -> List.rev ids, avoid - | app, (_, (Name id, _, _)) :: need when List.mem_assoc id named -> - aux (List.assoc id named :: ids) avoid app need + | app, (_, (Name id, _, _)) :: need + when List.mem_assoc_f Id.equal id named -> + aux (List.assoc_f Id.equal id named :: ids) avoid app need | (x, None) :: app, (None, (Name id, _, _)) :: need -> aux (x :: ids) avoid app need diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0e4cd80df..50cbcd605 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -22,6 +22,14 @@ open Decl_kinds (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) +module IdList = struct + let assoc id l = List.assoc_f Id.equal id l + let remove_assoc id l = List.remove_assoc_f Id.equal id l + let mem id l = List.exists (Id.equal id) l + let mem_assoc id l = List.exists (fun (a,_) -> Id.equal id a) l + let rev_mem_assoc id l = List.exists (fun (_,b) -> Id.equal id b) l +end + let name_to_ident = function | Anonymous -> Errors.error "This expression should be a simple identifier." | Name id -> id @@ -37,15 +45,15 @@ let rec cases_pattern_fold_map loc g e = function e', PatCstr (loc,cstr,patl',na') let rec subst_glob_vars l = function - | GVar (_,id) as r -> (try List.assoc id l with Not_found -> r) + | GVar (_,id) as r -> (try IdList.assoc id l with Not_found -> r) | GProd (loc,Name id,bk,t,c) -> let id = - try match List.assoc id l with GVar(_,id') -> id' | _ -> id + try match IdList.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) | GLambda (loc,Name id,bk,t,c) -> let id = - try match List.assoc id l with GVar(_,id') -> id' | _ -> id + try match IdList.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c) | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *) @@ -298,31 +306,34 @@ let notation_constr_and_vars_of_glob_constr a = (* Side effect *) t, !found -let rec list_rev_mem_assoc x = function - | [] -> false - | (_,x')::l -> Id.equal x x' || list_rev_mem_assoc x l +let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' let check_variables vars recvars (found,foundrec,foundrecbinding) = let fold _ y accu = Id.Set.add y accu in let useless_vars = Id.Map.fold fold recvars Id.Set.empty in let vars = Id.Map.filter (fun y _ -> not (Id.Set.mem y useless_vars)) vars in let check_recvar x = - if List.mem x found then + if IdList.mem x found then errorlabstrm "" (pr_id x ++ strbrk " should only be used in the recursive part of a pattern.") in let check (x, y) = check_recvar x; check_recvar y in let () = List.iter check foundrec in let () = List.iter check foundrecbinding in let check_bound x = - if not (List.mem x found) then - if List.mem_assoc x foundrec || List.mem_assoc x foundrecbinding - || list_rev_mem_assoc x foundrec || list_rev_mem_assoc x foundrecbinding + if not (IdList.mem x found) then + if IdList.mem_assoc x foundrec || + IdList.mem_assoc x foundrecbinding || + IdList.rev_mem_assoc x foundrec || + IdList.rev_mem_assoc x foundrecbinding then - error ((Id.to_string x)^" should not be bound in a recursive pattern of the right-hand side.") + error + (Id.to_string x ^ + " should not be bound in a recursive pattern of the right-hand side.") else - error ((Id.to_string x)^" is unbound in the right-hand side.") in + error (Id.to_string x ^ " is unbound in the right-hand side.") + in let check_pair s x y where = - if not (List.mem (x,y) where) then + if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++ str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in @@ -515,11 +526,11 @@ let add_env alp (sigma,sigmalist,sigmabinders) var v = let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = try - let v' = List.assoc var sigma in + let v' = IdList.assoc var sigma in match v, v' with | GHole _, _ -> fullsigma | _, GHole _ -> - add_env alp (List.remove_assoc var sigma,sigmalist,sigmabinders) var v + add_env alp (IdList.remove_assoc var sigma,sigmalist,sigmabinders) var v | _, _ -> if Pervasives.(=) v v' then fullsigma (** FIXME *) else raise No_match @@ -547,7 +558,7 @@ let match_opt f sigma t1 t2 = match (t1,t2) with | _ -> raise No_match let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with - | (_,Name id2) when List.mem id2 (fst metas) -> + | (_,Name id2) when IdList.mem id2 (fst metas) -> let rhs = match na1 with | Name id1 -> GVar (Loc.ghost,id1) | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole) in @@ -578,14 +589,16 @@ let rec match_iterated_binders islambda decls = function | b -> (decls,b) let remove_sigma x (sigmavar,sigmalist,sigmabinders) = - (List.remove_assoc x sigmavar,sigmalist,sigmabinders) + (IdList.remove_assoc x sigmavar,sigmalist,sigmabinders) let match_abinderlist_with_app match_fun metas sigma rest x iter termin = let rec aux sigma acc rest = try let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = List.assoc ldots_var (pi1 sigma) in - let b = match List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false in + let rest = IdList.assoc ldots_var (pi1 sigma) in + let b = + match IdList.assoc x (pi3 sigma) with [b] -> b | _ ->assert false + in let sigma = remove_sigma x (remove_sigma ldots_var sigma) in aux sigma (b::acc) rest with No_match when not (List.is_empty acc) -> @@ -597,8 +610,8 @@ let match_alist match_fun metas sigma rest x iter termin lassoc = let rec aux sigma acc rest = try let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = List.assoc ldots_var (pi1 sigma) in - let t = List.assoc x (pi1 sigma) in + let rest = IdList.assoc ldots_var (pi1 sigma) in + let t = IdList.assoc x (pi1 sigma) in let sigma = remove_sigma x (remove_sigma ldots_var sigma) in aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> @@ -622,7 +635,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = match (a1,a2) with (* Matching notation variable *) - | r1, NVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1 + | r1, NVar id2 when IdList.mem id2 tmetas -> bind_env alp sigma id2 r1 (* Matching recursive notations for terms *) | r1, NList (x,_,iter,termin,lassoc) -> @@ -643,10 +656,10 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin (* Matching individual binders as part of a recursive pattern *) - | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when List.mem id blmetas -> + | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when IdList.mem id blmetas -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) - when List.mem id blmetas && na != Anonymous -> + when IdList.mem id blmetas && na != Anonymous -> match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 (* Matching compositionally *) @@ -760,7 +773,7 @@ let match_notation_constr u c (metas,pat) = let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in (* Reorder canonically the substitution *) let find x = - try List.assoc x terms + try IdList.assoc x terms with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) @@ -770,9 +783,9 @@ let match_notation_constr u c (metas,pat) = | NtnTypeConstr -> ((find x, scl)::terms',termlists',binders') | NtnTypeConstrList -> - (terms',(List.assoc x termlists,scl)::termlists',binders') + (terms',(IdList.assoc x termlists,scl)::termlists',binders') | NtnTypeBinderList -> - (terms',termlists',(List.assoc x binders,scl)::binders')) + (terms',termlists',(IdList.assoc x binders,scl)::binders')) metas ([],[],[]) (* Matching cases pattern *) @@ -783,7 +796,7 @@ let add_patterns_for_params ind l = let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = try - let vvar = List.assoc var sigma in + let vvar = IdList.assoc var sigma in if Pervasives.(=) v vvar then fullsigma else raise No_match (** FIXME *) with Not_found -> (* TODO: handle the case of multiple occs in different scopes *) @@ -791,7 +804,7 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with - | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) + | r1, NVar id2 when IdList.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> sigma,(0,add_patterns_for_params (fst r1) largs) @@ -833,8 +846,8 @@ let match_ind_pattern metas sigma ind pats a2 = let reorder_canonically_substitution terms termlists metas = List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> match typ with - | NtnTypeConstr -> ((List.assoc x terms, scl)::terms',termlists') - | NtnTypeConstrList -> (terms',(List.assoc x termlists,scl)::termlists') + | NtnTypeConstr -> ((IdList.assoc x terms, scl)::terms',termlists') + | NtnTypeConstrList -> (terms',(IdList.assoc x termlists,scl)::termlists') | NtnTypeBinderList -> assert false) metas ([],[]) diff --git a/kernel/closure.ml b/kernel/closure.ml index 28818de1f..a32be4f69 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -246,7 +246,7 @@ let ref_value_cache info ref = | None -> raise Not_found | Some t -> lift n t end - | VarKey id -> List.assoc id info.i_vars + | VarKey id -> List.assoc_f Id.equal id info.i_vars | ConstKey cst -> constant_value info.i_env cst in let v = info.i_repr info body in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d52877fd2..e564feb69 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -123,7 +123,9 @@ let sort_as_univ = function | Prop Pos -> type0_univ let cons_subst u su subst = - try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst + try + (u, sup su (List.assoc_f Universe.equal u subst)) :: + List.remove_assoc_f Universe.equal u subst with Not_found -> (u, su) :: subst let actualize_decl_level env lev t = diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index fbee52dd7..874e4a573 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -615,14 +615,14 @@ let get_rel env id i = List.nth env.env_rel (i-1) else let i = i - env.env_bound in - try List.assoc i !(env.env_urel) + try List.assoc_f Int.equal i !(env.env_urel) with Not_found -> let local = MLlocal (fresh_lname id) in env.env_urel := (i,local) :: !(env.env_urel); local let get_var env id = - try List.assoc id !(env.env_named) + try List.assoc_f Id.equal id !(env.env_named) with Not_found -> let local = MLlocal (fresh_lname (Name id)) in env.env_named := (id, local)::!(env.env_named); diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 90d52572a..40f16a6e6 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -254,7 +254,7 @@ let check_initial senv = assert (is_initial senv) let check_imports current_libs needed = let check (id,stamp) = try - let actual_stamp = List.assoc id current_libs in + let actual_stamp = List.assoc_f DirPath.equal id current_libs in if not (String.equal stamp actual_stamp) then Errors.error ("Inconsistent assumptions over module "^(DirPath.to_string id)^".") diff --git a/lib/cList.ml b/lib/cList.ml index db2aa2bcf..6559efd40 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -131,6 +131,7 @@ sig val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list + val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val cartesians : ('a -> 'b -> 'b) -> 'b -> 'a list list -> 'b list val combinations : 'a list list -> 'a list list @@ -735,7 +736,9 @@ let rec assoc_f f a = function | (x, e) :: xs -> if f a x then e else assoc_f f a xs | [] -> raise Not_found -let remove_assoc_f f a l = remove_first (fun (x,y) -> f a x) l +let remove_assoc_f f a l = remove_first (fun (x,_) -> f a x) l + +let mem_assoc_f f a l = List.exists (fun (x,_) -> f a x) l (* A generic cartesian product: for any operator (**), [cartesian (**) [x1;x2] [y1;y2] = [x1**y1; x1**y2; x2**y1; x2**y1]], diff --git a/lib/cList.mli b/lib/cList.mli index 60110228a..3968a4adf 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -217,6 +217,7 @@ sig val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list + val mem_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> bool val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list (** A generic cartesian product: for any operator (**), diff --git a/library/goptions.ml b/library/goptions.ml index d38d2762a..87c387080 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -121,7 +121,7 @@ module MakeTable = let string_table = ref [] -let get_string_table k = List.assoc (nickname k) !string_table +let get_string_table k = List.assoc_f String.equal (nickname k) !string_table module type StringConvertArg = sig @@ -150,7 +150,7 @@ module MakeStringTable = let ref_table = ref [] -let get_ref_table k = List.assoc (nickname k) !ref_table +let get_ref_table k = List.assoc_f String.equal (nickname k) !ref_table module type RefConvertArg = sig diff --git a/library/impargs.ml b/library/impargs.ml index 66900ee42..61ea7a87a 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -352,8 +352,9 @@ let set_manual_implicits env flags enriching autoimps l = | (Name id,imp)::imps -> let l',imp,m = try - let (b, fi, fo) = List.assoc (ExplByName id) l in - List.remove_assoc (ExplByName id) l, (Some Manual), (Some (b, fi)) + let eq = (Pervasives.(=) : explicitation -> explicitation -> bool) in (* FIXME *) + let (b, fi, fo) = List.assoc_f eq (ExplByName id) l in + List.remove_assoc_f eq (ExplByName id) l, (Some Manual), (Some (b, fi)) with Not_found -> try let (id, (b, fi, fo)), l' = assoc_by_pos k l in diff --git a/library/library.ml b/library/library.ml index a15b66d20..09968c5ae 100644 --- a/library/library.ml +++ b/library/library.ml @@ -232,8 +232,11 @@ let locate_qualified_library warn qid = let loadpath = Loadpath.expand_path dir in let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in let name = Id.to_string base ^ ".vo" in - let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in - let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in + let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name + in + let dir = + add_dirpath_suffix (List.assoc_f String.equal lpath loadpath) base + in (* Look if loaded *) if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) @@ -382,7 +385,7 @@ let rec intern_library needed (dir, f) = try find_library dir, needed with Not_found -> (* Look if already listed and consequently its dependencies too *) - try List.assoc dir needed, needed + try List.assoc_f DirPath.equal dir needed, needed with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 6e6612e9a..959dba132 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -74,7 +74,7 @@ let nmtoken (loc,a) = with Failure _ -> user_err_loc (loc,"",str "nmtoken expected.") let get_xml_attr s al = - try List.assoc s al + try List.assoc_f String.equal s al with Not_found -> error ("No attribute "^s) (* Interpreting specific attributes *) @@ -124,7 +124,7 @@ let get_xml_constructor al = (get_xml_inductive al, nmtoken (get_xml_attr "noConstr" al)) let get_xml_binder al = - try Name (ident_of_cdata (List.assoc "binder" al)) + try Name (ident_of_cdata (List.assoc_f String.equal "binder" al)) with Not_found -> Anonymous let get_xml_ident al = ident_of_cdata (get_xml_attr "binder" al) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 8060dcabf..01f90f6c6 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -278,7 +278,8 @@ let rec bind_primary_aliases map pat = List.fold_left bind_primary_aliases map1 lpat let bind_secondary_aliases map subst = - Id.Map.fold (fun ids (idp : Id.t) map -> (ids,List.assoc idp map)::map) subst map + Id.Map.fold + (fun ids idp map -> (ids,List.assoc_f Id.equal idp map)::map) subst map let bind_aliases patvars subst patt = let map = bind_primary_aliases [] patt in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e18df6e46..673b749e1 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1189,7 +1189,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = execute_cases fix_name per_info tacnext args0 next_objs nhrec t gls | End_patt (id,(nparams,nhyps)),[] -> begin - match List.assoc id args with + match List.assoc_f Id.equal id args with [None,br_args] -> let all_metas = List.init (nparams + nhyps) (fun n -> mkMeta (succ n)) in diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 45977b657..e6bcefe22 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -213,7 +213,7 @@ let get_decl_in_structure r struc = try let base_mp,ll = labels_of_ref r in if not (at_toplevel base_mp) then error_not_visible r; - let sel = List.assoc base_mp struc in + let sel = List.assoc_f ModPath.equal base_mp struc in let rec go ll sel = match ll with | [] -> assert false | l :: ll -> diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index eeaf270c3..083108bef 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -32,7 +32,7 @@ let unif t1 t2= match kind_of_term t with Meta i-> (try - head_reduce (List.assoc i !sigma) + head_reduce (List.assoc_f Int.equal i !sigma) with Not_found->t) | _->t in Queue.add (t1,t2) bige; @@ -105,7 +105,7 @@ let mk_rel_inst t= match kind_of_term t with Meta n-> (try - mkRel (d+(List.assoc n !rel_env)) + mkRel (d+(List.assoc_f Int.equal n !rel_env)) with Not_found-> let m= !new_rel in incr new_rel; @@ -117,7 +117,7 @@ let mk_rel_inst t= let unif_atoms i dom t1 t2= try - let t=List.assoc i (unif t1 t2) in + let t=List.assoc_f Int.equal i (unif t1 t2) in if isMeta t then Some (Phantom dom) else Some (Real(mk_rel_inst t,value i t1)) with diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 58f43ed49..e5d8fe4c1 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -482,7 +482,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in List.map - (function const -> List.assoc const this_block_funs_indexes) + (function cst -> List.assoc_f Constant.equal cst this_block_funs_indexes) funs in let ind_list = @@ -665,7 +665,7 @@ let build_case_scheme fa = let prop_sort = InProp in let funs_indexes = let this_block_funs_indexes = Array.to_list this_block_funs_indexes in - List.assoc (destConst funs) this_block_funs_indexes + List.assoc_f Constant.equal (destConst funs) this_block_funs_indexes in let ind_fun = let ind = first_fun_kn,funs_indexes in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 96a60424c..57019b3fa 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -701,7 +701,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ = args; begin try - let v = List.assoc args expr_info.args_assoc in + let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in let new_infos = {expr_info with info = v} in tclTHENLIST[ continuation_tac new_infos; @@ -951,7 +951,7 @@ let equation_app f_and_args expr_info continuation_tac infos = let equation_app_rec (f,args) expr_info continuation_tac info = begin try - let v = List.assoc args expr_info.args_assoc in + let v = List.assoc_f (List.equal Constr.equal) args expr_info.args_assoc in let new_infos = {expr_info with info = v} in observe_tac (str "app_rec found") (continuation_tac new_infos) with Not_found -> diff --git a/plugins/micromega/sos.ml b/plugins/micromega/sos.ml index eb3d81901..c8957f4cd 100644 --- a/plugins/micromega/sos.ml +++ b/plugins/micromega/sos.ml @@ -1377,7 +1377,7 @@ let allvarorders l = List.map (fun vlis x -> index x vlis) (allpermutations l);; let changevariables_monomial zoln (m:monomial) = - foldl (fun a x k -> (List.assoc x zoln |-> k) a) monomial_1 m;; + foldl (fun a x k -> (List.assoc_f (=) x zoln |-> k) a) monomial_1 m;; let changevariables zoln pol = foldl (fun a m c -> (changevariables_monomial zoln m |-> c) a) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index c39b2ff0a..5c057231a 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -131,20 +131,24 @@ let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s] let rev_assoc k = let rec loop = function - | [] -> raise Not_found | (v,k')::_ when Int.equal k k' -> v | _ :: l -> loop l + | [] -> raise Not_found + | (v,k')::_ when Int.equal k k' -> v + | _ :: l -> loop l in loop let tag_hypothesis,tag_of_hyp, hyp_of_tag = let l = ref ([]:(Id.t * int) list) in (fun h id -> l := (h,id):: !l), - (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"), + (fun h -> + try List.assoc_f Id.equal h !l with Not_found -> failwith "tag_hypothesis"), (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis") let hide_constr,find_constr,clear_tables,dump_tables = let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), - (fun h -> try List.assoc_f eq_constr h !l with Not_found -> failwith "find_contr"), + (fun h -> + try List.assoc_f Constr.equal h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) @@ -1018,7 +1022,7 @@ let replay_history tactic_normalisation = begin try tclTHEN - (List.assoc (hyp_of_tag e.id) tactic_normalisation) + (List.assoc_f Id.equal (hyp_of_tag e.id) tactic_normalisation) (loop l) with Not_found -> loop l end | NEGATE_CONTRADICT (e2,e1,b) :: l -> diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml index cf1a7e6db..b74faf30b 100644 --- a/plugins/omega/omega.ml +++ b/plugins/omega/omega.ml @@ -705,7 +705,7 @@ let simplify_strong ((new_eq_id,new_var_id,print_var) as new_ids) system = let s2' = List.map remove_int s2 in let (r1,relie1) = solve s1' and (r2,relie2) = solve s2' in - let (eq,id1,id2) = List.assoc id explode_map in + let (eq,id1,id2) = Util.List.assoc_f Int.equal id explode_map in [SPLIT_INEQ(eq,(id1,r1),(id2, r2))], eq.id :: Util.List.union Int.equal relie1 relie2 with FULL_SOLUTION (x0,x1) -> (x0,x1) diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 860a2524c..c5a0f798c 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -198,7 +198,7 @@ let display_omega_var i = Printf.sprintf "OV%d" i le terme d'un monome (le plus souvent un atome) *) let intern_omega env t = - begin try List.assoc t env.om_vars + begin try List.assoc_f Pervasives.(=) t env.om_vars (* FIXME *) with Not_found -> let v = new_omega_var () in env.om_vars <- (t,v) :: env.om_vars; v diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index f98625b64..26fab4ac2 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -188,7 +188,7 @@ let typeur sigma metamap = let rec type_of env cstr= match Term.kind_of_term cstr with | T.Meta n -> - (try T.strip_outer_cast (List.assoc n metamap) + (try T.strip_outer_cast (Util.List.assoc_f Int.equal n metamap) with Not_found -> Errors.anomaly ~label:"type_of" (Pp.str "this is not a well-typed term")) | T.Rel n -> let (_,_,ty) = Environ.lookup_rel n env in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c9f00c0cd..be62e65b3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1760,7 +1760,7 @@ let prepare_predicate_from_arsign_tycon loc tomatchs arsign c = | Rel n when n > lift -> (try (* Make the predicate dependent on the matched variable *) - let idx = List.assoc (n - lift) subst in + let idx = List.assoc_f Int.equal (n - lift) subst in mkRel (idx + lift) with Not_found -> (* A variable that is not matched, lift over the arsign. *) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 94119975a..fe3606ce4 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -221,7 +221,7 @@ let open_canonical_structure i (_,o) = let lo = compute_canonical_projections o in List.iter (fun ((proj,cs_pat),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in - let ocs = try Some (List.assoc cs_pat l) + let ocs = try Some (List.assoc_f Pervasives.(=) cs_pat l) (* FIXME *) with Not_found -> None in match ocs with | None -> object_table := Refmap.add proj ((cs_pat,s)::l) !object_table; @@ -287,7 +287,7 @@ let declare_canonical_structure ref = add_canonical_structure (check_and_decompose_canonical_structure ref) let lookup_canonical_conversion (proj,pat) = - List.assoc pat (Refmap.find proj !object_table) + List.assoc_f Pervasives.(=) pat (Refmap.find proj !object_table) (* FIXME *) let is_open_canonical_projection env sigma (c,args) = try diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 899def8c8..9ecf86698 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -625,7 +625,7 @@ type meta_value_map = (metavariable * constr) list let rec subst_meta bl c = match kind_of_term c with - | Meta i -> (try List.assoc i bl with Not_found -> c) + | Meta i -> (try List.assoc_f Int.equal i bl with Not_found -> c) | _ -> map_constr (subst_meta bl) c (* First utilities for avoiding telescope computation for subst_term *) diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 2b6684448..e19be4e12 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -960,7 +960,7 @@ and pr_extend s cl = try pr_gen a with Failure _ -> str ("<error in "^s^">") in try - let rls = List.assoc s (Egramml.get_extend_vernac_grammars()) in + let rls = List.assoc_f String.equal s (Egramml.get_extend_vernac_grammars()) in let rl = match_vernac_rule (List.map Genarg.genarg_tag cl) rls in let start,rl,cl = match rl with diff --git a/printing/printmod.ml b/printing/printmod.ml index b5d1d8a18..b5f84c79e 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -46,7 +46,7 @@ let get_new_id locals id = get_id (List.map snd locals) id let rec print_local_modpath locals = function - | MPbound mbid -> pr_id (List.assoc mbid locals) + | MPbound mbid -> pr_id (Util.List.assoc_f MBId.equal mbid locals) | MPdot(mp,l) -> print_local_modpath locals mp ++ str "." ++ pr_lab l | MPfile _ -> raise Not_found diff --git a/toplevel/command.ml b/toplevel/command.ml index 127d1d76e..56a370155 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -95,11 +95,16 @@ let interp_definition bl red_option c ctypopt = let body = nf_evar !evdref (it_mkLambda_or_LetIn c ctx) in let typ = nf_evar !evdref (it_mkProd_or_LetIn ty ctx) in let beq b1 b2 = if b1 then b2 else not b2 in - let impl_eq (x1, y1, z1) (x2, y2, z2) = beq x1 x2 && beq y1 y2 && beq z1 z2 in - (* Check that all implicit arguments inferable from the term is inferable from the type *) - if not (try List.for_all (fun (key,va) -> impl_eq (List.assoc key impsty) va) imps2 with Not_found -> false) - then msg_warning (strbrk "Implicit arguments declaration relies on type." ++ - spc () ++ strbrk "The term declares more implicits than the type here."); + let impl_eq (x,y,z) (x',y',z') = beq x x' && beq y y' && beq z z' in + (* Check that all implicit arguments inferable from the term + are inferable from the type *) + let chk (key,va) = + impl_eq (List.assoc_f Pervasives.(=) key impsty) va (* FIXME *) + in + if not (try List.for_all chk imps2 with Not_found -> false) + then msg_warning + (strbrk "Implicit arguments declaration relies on type." ++ spc () ++ + strbrk "The term declares more implicits than the type here."); imps1@(Impargs.lift_implicits nb_args impsty), { const_entry_body = Future.from_val(body,Declareops.no_seff); const_entry_secctx = None; diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 45621ced8..5846c73a8 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -149,7 +149,7 @@ let define_mutual_scheme_base kind suff f internal names mind = let cl, eff = f mind in let mib = Global.lookup_mind mind in let ids = Array.init (Array.length mib.mind_packets) (fun i -> - try List.assoc i names + try List.assoc_f Int.equal i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let consts = Array.map2 (define internal) ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 0a21b6d6e..b6e86a212 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -65,7 +65,7 @@ let evar_tactic = Store.field () let subst_evar_constr evs n idf t = let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in - let evar_info id = List.assoc id evs in + let evar_info id = List.assoc_f Evar.equal id evs in let rec substrec (depth, fixrels) c = match kind_of_term c with | Evar (k, args) -> let { ev_name = (id, idstr) ; @@ -425,7 +425,7 @@ let replace_appvars subst = if isVar f then try let c' = List.map (map_constr aux) l in - let (t, b) = List.assoc (destVar f) subst in + let (t, b) = List.assoc_f Id.equal (destVar f) subst in mkApp (delayed_force hide_obligation, [| prod_applist t c'; applistc b c' |]) with Not_found -> map_constr aux c |