diff options
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/cc/cctac.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/common.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 1 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 6 | ||||
-rw-r--r-- | plugins/firstorder/instances.ml | 4 | ||||
-rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
-rw-r--r-- | plugins/funind/functional_principles_types.ml | 4 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 48 | ||||
-rw-r--r-- | plugins/funind/glob_termops.ml | 18 | ||||
-rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 12 | ||||
-rw-r--r-- | plugins/funind/merge.ml | 4 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 10 | ||||
-rw-r--r-- | plugins/ltac/evar_tactics.ml | 2 | ||||
-rw-r--r-- | plugins/ltac/extratactics.ml4 | 4 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 10 | ||||
-rw-r--r-- | plugins/ltac/rewrite.ml | 4 | ||||
-rw-r--r-- | plugins/ltac/rewrite.mli | 2 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.ml | 30 | ||||
-rw-r--r-- | plugins/ltac/tacinterp.mli | 4 | ||||
-rw-r--r-- | plugins/micromega/coq_micromega.ml | 4 | ||||
-rw-r--r-- | plugins/omega/coq_omega.ml | 6 | ||||
-rw-r--r-- | plugins/ssr/ssrequality.ml | 2 | ||||
-rw-r--r-- | plugins/ssr/ssrparser.ml4 | 2 |
24 files changed, 96 insertions, 91 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index fca7d9851..150319f6b 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -444,7 +444,7 @@ let cc_tactic depth additionnal_terms = let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in let pr_missing (c, missing) = - let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in + let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in let holes = List.init missing (fun _ -> hole) in Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes)) in diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9772ebd64..9aec190d0 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -405,7 +405,7 @@ let ref_renaming_fun (k,r) = let idg = safe_basename_of_global r in match l with | [""] -> (* this happens only at toplevel of the monolithic case *) - let globs = Id.Set.elements (get_global_ids ()) in + let globs = get_global_ids () in let id = next_ident_away (kindcase_id k idg) globs in Id.to_string id | _ -> modular_rename k idg diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 7644b49ce..a227478d0 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -141,6 +141,7 @@ let make_typvar n vl = if not (String.contains s '\'') && Unicode.is_basic_ascii s then id else id_of_name Anonymous in + let vl = Id.Set.of_list vl in next_ident_away id' vl let rec type_sign_vl env c = diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ca98f07e8..30e3b520f 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -750,11 +750,11 @@ let extraction_implicit r l = let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist" -let modfile_ids = ref [] +let modfile_ids = ref Id.Set.empty let modfile_mps = ref MPmap.empty let reset_modfile () = - modfile_ids := Id.Set.elements !blacklist_table; + modfile_ids := !blacklist_table; modfile_mps := MPmap.empty let string_of_modfile mp = @@ -763,7 +763,7 @@ let string_of_modfile mp = let id = Id.of_string (raw_string_of_modfile mp) in let id' = next_ident_away id !modfile_ids in let s' = Id.to_string id' in - modfile_ids := id' :: !modfile_ids; + modfile_ids := Id.Set.add id' !modfile_ids; modfile_mps := MPmap.add mp s' !modfile_mps; s' diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 169073630..c2606dbe8 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -115,8 +115,8 @@ let mk_open_instance env evmap id idc m t = let nid=(fresh_id_in_env avoid var_id env) in let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in let decl = LocalAssum (Name nid, c) in - aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in - let evmap, decls = aux m [] env evmap [] in + aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in + let evmap, decls = aux m Id.Set.empty env evmap [] in (evmap, decls, revt) (* tactics *) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 5f6d78359..bd5fb1d92 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -587,7 +587,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = tclTHENLIST [ (* We first introduce the variables *) - tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding dyn_infos.rec_hyps)); + tclDO nb_first_intro (Proofview.V82.of_tactic (intro_avoiding (Id.Set.of_list dyn_infos.rec_hyps))); (* Then the equation itself *) Proofview.V82.of_tactic (intro_using heq_id); onLastHypId (fun heq_id -> tclTHENLIST [ @@ -1614,7 +1614,7 @@ let prove_principle_for_gen let hid = next_ident_away_in_goal (Id.of_string "prov") - hyps + (Id.Set.of_list hyps) in tclTHENLIST [ diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 409bb89ee..018b51517 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -39,7 +39,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = | decl :: predicates -> (match Context.Rel.Declaration.get_name decl with | Name x -> - let id = Namegen.next_ident_away x avoid in + let id = Namegen.next_ident_away x (Id.Set.of_list avoid) in Hashtbl.add tbl id x; RelDecl.set_name (Name id) decl :: change_predicates_names (id::avoid) predicates | Anonymous -> anomaly (Pp.str "Anonymous property binder.")) @@ -285,7 +285,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin (* let time2 = System.get_time () in *) (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *) let new_princ_name = - next_ident_away_in_goal (Id.of_string "___________princ_________") [] + next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty in let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in let hook = Lemmas.mk_hook (hook new_principle_type) in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 7087a195e..e8e5bfccc 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -120,13 +120,13 @@ let combine_args arg args = let ids_of_binder = function - | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> [] - | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> [id] + | LetIn Anonymous | Prod Anonymous | Lambda Anonymous -> Id.Set.empty + | LetIn (Name id) | Prod (Name id) | Lambda (Name id) -> Id.Set.singleton id let rec change_vars_in_binder mapping = function [] -> [] | (bt,t)::l -> - let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in + let new_mapping = Id.Set.fold Id.Map.remove (ids_of_binder bt) mapping in (bt,change_vars mapping t):: (if Id.Map.is_empty new_mapping then l @@ -137,27 +137,27 @@ let rec replace_var_by_term_in_binder x_id term = function | [] -> [] | (bt,t)::l -> (bt,replace_var_by_term x_id term t):: - if Id.List.mem x_id (ids_of_binder bt) + if Id.Set.mem x_id (ids_of_binder bt) then l else replace_var_by_term_in_binder x_id term l -let add_bt_names bt = List.append (ids_of_binder bt) +let add_bt_names bt = Id.Set.union (ids_of_binder bt) let apply_args ctxt body args = let need_convert_id avoid id = - List.exists (is_free_in id) args || Id.List.mem id avoid + List.exists (is_free_in id) args || Id.Set.mem id avoid in let need_convert avoid bt = - List.exists (need_convert_id avoid) (ids_of_binder bt) + Id.Set.exists (need_convert_id avoid) (ids_of_binder bt) in - let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.t list) = + let next_name_away (na:Name.t) (mapping: Id.t Id.Map.t) (avoid: Id.Set.t) = match na with - | Name id when Id.List.mem id avoid -> + | Name id when Id.Set.mem id avoid -> let new_id = Namegen.next_ident_away id avoid in - Name new_id,Id.Map.add id new_id mapping,new_id::avoid + Name new_id,Id.Map.add id new_id mapping,Id.Set.add new_id avoid | _ -> na,mapping,avoid in - let next_bt_away bt (avoid:Id.t list) = + let next_bt_away bt (avoid:Id.Set.t) = match bt with | LetIn na -> let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid in @@ -182,15 +182,15 @@ let apply_args ctxt body args = let new_avoid,new_ctxt',new_body,new_id = if need_convert_id avoid id then - let new_avoid = id::avoid in + let new_avoid = Id.Set.add id avoid in let new_id = Namegen.next_ident_away id new_avoid in - let new_avoid' = new_id :: new_avoid in + let new_avoid' = Id.Set.add new_id new_avoid in let mapping = Id.Map.add id new_id Id.Map.empty in let new_ctxt' = change_vars_in_binder mapping ctxt' in let new_body = change_vars mapping body in new_avoid',new_ctxt',new_body,new_id else - id::avoid,ctxt',body,id + Id.Set.add id avoid,ctxt',body,id in let new_body = replace_var_by_term new_id arg new_body in let new_ctxt' = replace_var_by_term_in_binder new_id arg new_ctxt' in @@ -214,7 +214,7 @@ let apply_args ctxt body args = in (new_bt,t)::new_ctxt',new_body in - do_apply [] ctxt body args + do_apply Id.Set.empty ctxt body args let combine_app f args = @@ -434,7 +434,7 @@ let rec pattern_to_term_and_type env typ = DAst.with_val (function Array.to_list (Array.init (cst_narg - List.length patternl) - (fun i -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr csta.(i))) + (fun i -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr csta.(i))) ) in let patl_as_term = @@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = *) let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in - let res_raw_type = Detyping.detype Detyping.Now false [] env (Evd.from_env env) rt_typ in + let res_raw_type = Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) rt_typ in let res = fresh_id args_res.to_avoid "_res" in let new_avoid = res::args_res.to_avoid in let res_rt = mkGVar res in @@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = match n with | Name id when List.exists (is_free_in id) args -> (* need to alpha-convert the name *) - let new_id = Namegen.next_ident_away id avoid in + let new_id = Namegen.next_ident_away id (Id.Set.of_list avoid) in let new_avoid = id:: avoid in let new_b = replace_var_by_term @@ -773,7 +773,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype Detyping.Now false [] + Detyping.detype Detyping.Now false Id.Set.empty env_with_pat_ids (Evd.from_env env) typ_of_id in mkGProd (Name id,raw_typ_of_id,acc)) @@ -819,7 +819,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve (fun pat e typ_as_constr -> let this_pat_ids = ids_of_pat pat in let typ_as_constr = EConstr.of_constr typ_as_constr in - let typ = Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_as_constr in + let typ = Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in (* removing trivial holes *) let pat_as_term = solve_trivial_holes pat_as_term e in @@ -833,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve then (Prod (Name id), let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in let raw_typ_of_id = - Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_of_id + Detyping.detype Detyping.Now false Id.Set.empty new_env (Evd.from_env env) typ_of_id in raw_typ_of_id )::acc @@ -1001,7 +1001,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = let rt_typ = DAst.make @@ GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None), (List.map - (fun p -> Detyping.detype Detyping.Now false [] + (fun p -> Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) (EConstr.of_constr p)) params)@(Array.to_list (Array.make @@ -1028,12 +1028,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match na with | Anonymous -> acc | Name id' -> - (id',Detyping.detype Detyping.Now false [] + (id',Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) arg)::acc else if isVar var_as_constr - then (destVar var_as_constr,Detyping.detype Detyping.Now false [] + then (destVar var_as_constr,Detyping.detype Detyping.Now false Id.Set.empty env (Evd.from_env env) arg)::acc diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 02ee56ac5..0666ab4f1 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -198,7 +198,7 @@ let rec alpha_pat excluded pat = | PatVar(Name id) -> if Id.List.mem id excluded then - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded), (Id.Map.add id new_id Id.Map.empty) else pat, excluded,Id.Map.empty @@ -206,7 +206,7 @@ let rec alpha_pat excluded pat = let new_na,new_excluded,map = match na with | Name id when Id.List.mem id excluded -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty | _ -> na,excluded,Id.Map.empty in @@ -261,7 +261,7 @@ let rec alpha_rt excluded rt = match DAst.get rt with | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt | GLambda(Anonymous,k,t,b) -> - let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in + let new_id = Namegen.next_ident_away (Id.of_string "_x") (Id.Set.of_list excluded) in let new_excluded = new_id :: excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in @@ -276,7 +276,7 @@ let rec alpha_rt excluded rt = let new_c = alpha_rt excluded c in GLetIn(Anonymous,new_b,new_t,new_c) | GLambda(Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let t,b = if Id.equal new_id id then t, b @@ -289,7 +289,7 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in GLambda(Name new_id,k,new_t,new_b) | GProd(Name id,k,t,b) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let new_excluded = new_id::excluded in let t,b = if Id.equal new_id id @@ -302,7 +302,7 @@ let rec alpha_rt excluded rt = let new_b = alpha_rt new_excluded b in GProd(Name new_id,k,new_t,new_b) | GLetIn(Name id,b,t,c) -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in let c = if Id.equal new_id id then c else change_vars (Id.Map.add id new_id Id.Map.empty) c @@ -320,7 +320,7 @@ let rec alpha_rt excluded rt = match na with | Anonymous -> (na::nal,excluded,mapping) | Name id -> - let new_id = Namegen.next_ident_away id excluded in + let new_id = Namegen.next_ident_away id (Id.Set.of_list excluded) in if Id.equal new_id id then na::nal,id::excluded,mapping @@ -741,7 +741,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) @@ -763,7 +763,7 @@ If someone knows how to prevent solved existantial removal in understand, pleas match evi.evar_body with | Evar_defined c -> (* we just have to lift the solution in glob_term *) - Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c)) + Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) in res diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 5f4d514f3..1e8854249 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -12,7 +12,7 @@ let mk_equation_id id = Nameops.add_suffix id "_equation" let msgnl m = () -let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid +let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) (Id.Set.of_list avoid) let fresh_name avoid s = Name (fresh_id avoid s) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 5f8d50da1..299753766 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -131,9 +131,9 @@ let generate_type evd g_to_f f graph i = | Name id -> Some id | Anonymous -> None in - let named_ctxt = List.map_filter filter fun_ctxt in + let named_ctxt = Id.Set.of_list (List.map_filter filter fun_ctxt) in let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in - let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in + let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (Id.Set.add res_id named_ctxt) in (*i we can then type the argument to be applied to the function [f] i*) let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in (*i @@ -189,7 +189,7 @@ let rec generate_fresh_id x avoid i = if i == 0 then [] else - let id = Namegen.next_ident_away_in_goal x avoid in + let id = Namegen.next_ident_away_in_goal x (Id.Set.of_list avoid) in id::(generate_fresh_id x (id::avoid) (pred i)) @@ -239,7 +239,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes environment and due to the bug #1174, we will need to pose the principle using a name *) - let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in + let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") (Id.Set.of_list ids) in let ids = principle_id :: ids in (* We get the branches of the principle *) let branches = List.rev princ_infos.branches in @@ -396,7 +396,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.Name.get_id (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -406,7 +406,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.Name.get_id (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) (Id.Set.of_list avoid) in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 96200a98a..77c26f8ce 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -767,7 +767,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body) (* first replace rel 1 by a varname *) let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in let substindtyp = EConstr.of_constr substindtyp in - Detyping.detype Detyping.Now false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in + Detyping.detype Detyping.Now false avoid (Global.env()) Evd.empty substindtyp in let lcstr1: glob_constr list = Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in (* add to avoid all indentifiers of lcstr1 *) @@ -851,7 +851,7 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) = match rdecl with | LocalAssum (nme,t) -> let t = EConstr.of_constr t in - let traw = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in + let traw = Detyping.detype Detyping.Now false Id.Set.empty (Global.env()) Evd.empty t in DAst.make @@ GProd (nme,Explicit,traw,t2) | LocalDef _ -> assert false diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index d43fd78f3..6fcfec80d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -115,13 +115,17 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta (* Generic values *) let pf_get_new_ids idl g = let ids = pf_ids_of_hyps g in + let ids = Id.Set.of_list ids in List.fold_right - (fun id acc -> next_global_ident_away id (acc@ids)::acc) + (fun id acc -> next_global_ident_away id (Id.Set.union (Id.Set.of_list acc) ids)::acc) idl [] +let next_ident_away_in_goal ids avoid = + next_ident_away_in_goal ids (Id.Set.of_list avoid) + let compute_renamed_type gls c = - rename_bound_vars_as_displayed (project gls) (*no avoid*) [] (*no rels*) [] + rename_bound_vars_as_displayed (project gls) (*no avoid*) Id.Set.empty (*no rels*) [] (pf_unsafe_type_of gls c) let h'_id = Id.of_string "h'" let teq_id = Id.of_string "teq" @@ -1302,7 +1306,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp with e when CErrors.noncritical e -> anomaly (Pp.str "open_new_goal with an unamed theorem.") in - let na = next_global_ident_away name [] in + let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 4cab6ef33..be1d947d3 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -88,7 +88,7 @@ let let_evar name typ = let id = match name with | Name.Anonymous -> let id = Namegen.id_of_name_using_hdchar env sigma typ name in - Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) + Namegen.next_ident_away_in_goal id (Context.Named.to_vars (Environ.named_context env)) | Name.Name id -> id in let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index b4c6f9c90..a7aebf9e1 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -665,7 +665,7 @@ let hResolve id c occ t = let sigma = Proofview.Goal.sigma gl in let env = Termops.clear_named_body id (Proofview.Goal.env gl) in let concl = Proofview.Goal.concl gl in - let env_ids = Termops.ids_of_context env in + let env_ids = Termops.vars_of_env env in let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in let rec resolve_hole t_hole = @@ -764,7 +764,7 @@ let case_eq_intros_rewrite x = mkCaseEq x; Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in - let hyps = Tacmach.New.pf_ids_of_hyps gl in + let hyps = Tacmach.New.pf_ids_set_of_hyps gl in let n' = nb_prod (Tacmach.New.project gl) concl in let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in Tacticals.New.tclTHENLIST [ diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index f4e3ba633..8a0764975 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -662,14 +662,14 @@ type 'a extra_genarg_printer = let names = List.fold_left (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) + (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln) ln nal) - [] bll in + Id.Set.empty bll in let idarg,bll = set_nth_name names n bll in - let annot = match names with - | [_] -> + let annot = + if Int.equal (Id.Set.cardinal names) 1 then mt () - | _ -> + else spc() ++ str"{" ++ keyword "struct" ++ spc () ++ pr_id idarg ++ str"}" diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 3d01cbe8d..fd791a910 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -664,7 +664,7 @@ type rewrite_result = type 'a strategy_input = { state : 'a ; (* a parameter: for instance, a state *) env : Environ.env ; - unfresh : Id.t list ; (* Unfresh names *) + unfresh : Id.Set.t; (* Unfresh names *) term1 : constr ; ty1 : types ; (* first term and its type (convertible to rew_from) *) cstr : (bool (* prop *) * constr option) ; @@ -1614,7 +1614,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = in try let res = - cl_rewrite_clause_aux ?abs strat env [] sigma ty clause + cl_rewrite_clause_aux ?abs strat env Id.Set.empty sigma ty clause in let sigma = match origsigma with None -> sigma | Some sigma -> sigma in treat sigma res <*> diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 23767c12f..63e891b45 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -110,7 +110,7 @@ val setoid_transitivity : constr option -> unit Proofview.tactic val apply_strategy : strategy -> Environ.env -> - Names.Id.t list -> + Names.Id.Set.t -> constr -> bool * constr -> evars -> rewrite_result diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 8fa95ffb0..18348bc11 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -139,7 +139,7 @@ let name_vfun appl vle = module TacStore = Geninterp.TacStore -let f_avoid_ids : Id.t list TacStore.field = TacStore.field () +let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field () (* ids inherited from the call context (needed to get fresh ids) *) let f_debug : debug_info TacStore.field = TacStore.field () let f_trace : ltac_trace TacStore.field = TacStore.field () @@ -501,29 +501,29 @@ let extract_ltac_constr_values ist env = could barely be defined as a feature... *) (* Extract the identifier list from lfun: join all branches (what to do else?)*) -let rec intropattern_ids (loc,pat) = match pat with - | IntroNaming (IntroIdentifier id) -> [id] +let rec intropattern_ids accu (loc,pat) = match pat with + | IntroNaming (IntroIdentifier id) -> Id.Set.add id accu | IntroAction (IntroOrAndPattern (IntroAndPattern l)) -> - List.flatten (List.map intropattern_ids l) + List.fold_left intropattern_ids accu l | IntroAction (IntroOrAndPattern (IntroOrPattern ll)) -> - List.flatten (List.map intropattern_ids (List.flatten ll)) + List.fold_left intropattern_ids accu (List.flatten ll) | IntroAction (IntroInjection l) -> - List.flatten (List.map intropattern_ids l) - | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat + List.fold_left intropattern_ids accu l + | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids accu pat | IntroNaming (IntroAnonymous | IntroFresh _) | IntroAction (IntroWildcard | IntroRewrite _) - | IntroForthcoming _ -> [] + | IntroForthcoming _ -> accu -let extract_ids ids lfun = +let extract_ids ids lfun accu = let fold id v accu = let v = Value.normalize v in if has_type v (topwit wit_intro_pattern) then let (_, ipat) = out_gen (topwit wit_intro_pattern) v in if Id.List.mem id ids then accu - else accu @ intropattern_ids (Loc.tag ipat) + else intropattern_ids accu (Loc.tag ipat) else accu in - Id.Map.fold fold lfun [] + Id.Map.fold fold lfun accu let default_fresh_id = Id.of_string "H" @@ -534,10 +534,10 @@ let interp_fresh_id ist env sigma l = with Not_found -> id in let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with - | None -> [] + | None -> Id.Set.empty | Some l -> l in - let avoid = (extract_ids ids ist.lfun) @ avoid in + let avoid = extract_ids ids ist.lfun avoid in let id = if List.is_empty l then default_fresh_id else @@ -1303,7 +1303,7 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v end | ArgArg (loc,r) -> - let ids = extract_ids [] ist.lfun in + let ids = extract_ids [] ist.lfun Id.Set.empty in let loc_info = (Option.default loc loc',LtacNameCall r) in let extra = TacStore.set ist.extra f_avoid_ids ids in push_trace loc_info ist >>= fun trace -> @@ -1956,7 +1956,7 @@ let interp_tac_gen lfun avoid_ids debug t = (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t) end -let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t +let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index c1ab2b4c4..d0a0a81d4 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -40,7 +40,7 @@ type interp_sign = Geninterp.interp_sign = { lfun : value Id.Map.t; extra : TacStore.t } -val f_avoid_ids : Id.t list TacStore.field +val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field val extract_ltac_constr_values : interp_sign -> Environ.env -> @@ -113,7 +113,7 @@ val tactic_of_value : interp_sign -> Value.t -> unit Proofview.tactic (** Globalization + interpretation *) -val interp_tac_gen : value Id.Map.t -> Id.t list -> +val interp_tac_gen : value Id.Map.t -> Id.Set.t -> debug_info -> raw_tactic_expr -> unit Proofview.tactic val interp : raw_tactic_expr -> unit Proofview.tactic diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a4103634e..fc6781b06 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1986,7 +1986,7 @@ let micromega_gen let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in - let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in + let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; @@ -2101,7 +2101,7 @@ let micromega_genr prover tac = let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in - let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in + let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 99493d698..ae1a563be 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1760,7 +1760,7 @@ let onClearedName id tac = tclTHEN (tclTRY (clear [id])) (Proofview.Goal.nf_enter begin fun gl -> - let id = fresh_id [] id gl in + let id = fresh_id Id.Set.empty id gl in tclTHEN (introduction id) (tac id) end) @@ -1768,8 +1768,8 @@ let onClearedName2 id tac = tclTHEN (tclTRY (clear [id])) (Proofview.Goal.nf_enter begin fun gl -> - let id1 = fresh_id [] (add_suffix id "_left") gl in - let id2 = fresh_id [] (add_suffix id "_right") gl in + let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in + let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ] end) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 8b69c3435..95ca6f49a 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -129,7 +129,7 @@ let newssrcongrtac arg ist gl = let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in pf_saturate gl (EConstr.of_constr eq) 3 in tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args)) - (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) ty) ist) + (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist) (fun () -> let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 060225dab..1e1a986da 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -342,7 +342,7 @@ let interp_index ist gl idx = | None -> begin match Tacinterp.Value.to_constr v with | Some c -> - let rc = Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) c in + let rc = Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) c in begin match Notation.uninterp_prim_token rc with | _, Constrexpr.Numeral (s,b) -> let n = int_of_string s in if b then n else -n |