diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/auto.ml | 2 | ||||
-rw-r--r-- | tactics/class_tactics.ml4 | 16 | ||||
-rw-r--r-- | tactics/equality.ml | 10 | ||||
-rw-r--r-- | tactics/tactics.ml | 2 |
4 files changed, 15 insertions, 15 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 49841ecfa..ecc0930c1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -823,7 +823,7 @@ let prepare_hint env (sigma,c) = (* We skip the test whether args is the identity or not *) let t = Evarutil.nf_evar sigma (existential_type sigma ev) in let t = List.fold_right (fun (e,id) c -> replace_term e id c) !subst t in - if not (Intset.is_empty (free_rels t)) then + if not (Int.Set.is_empty (free_rels t)) then error "Hints with holes dependent on a bound variable not supported."; if occur_existential t then (* Not clever enough to construct dependency graph of evars *) diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index a18992f70..8e0dbc6ef 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -403,7 +403,7 @@ let isProp env sigma concl = let needs_backtrack only_classes env evd oev concl = if Option.is_empty oev || isProp env evd concl then - not (Intset.is_empty (Evarutil.evars_of_term concl)) + not (Int.Set.is_empty (Evarutil.evars_of_term concl)) else true let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = @@ -530,19 +530,19 @@ let resolve_all_evars_once debug limit p evd = Beware of the imperative effects on the partition structure, it should not be shared, but only used locally. *) -module Intpart = Unionfind.Make(Intset)(Intmap) +module Intpart = Unionfind.Make(Int.Set)(Int.Map) let deps_of_constraints cstrs evm p = List.iter (fun (_, _, x, y) -> let evx = Evarutil.undefined_evars_of_term evm x in let evy = Evarutil.undefined_evars_of_term evm y in - Intpart.union_set (Intset.union evx evy) p) + Intpart.union_set (Int.Set.union evx evy) p) cstrs let evar_dependencies evm p = Evd.fold_undefined (fun ev evi _ -> - let evars = Intset.add ev (Evarutil.undefined_evars_of_evar_info evm evi) + let evars = Int.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi) in Intpart.union_set evars p) evm () @@ -577,7 +577,7 @@ let split_evars evm = let evars_in_comp comp evm = try evars_reset_evd - (Intset.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev)) + (Int.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evm ev)) comp Evd.empty) evm with Not_found -> assert false @@ -595,7 +595,7 @@ let is_inference_forced p evd ev = with Not_found -> assert false let is_mandatory p comp evd = - Intset.exists (is_inference_forced p evd) comp + Int.Set.exists (is_inference_forced p evd) comp (** In case of unsatisfiable constraints, build a nice error message *) @@ -661,8 +661,8 @@ let revert_resolvability oevd evd = exception Unresolved let resolve_all_evars debug m env p oevd do_split fail = - let split = if do_split then split_evars oevd else [Intset.empty] in - let in_comp comp ev = if do_split then Intset.mem ev comp else true + let split = if do_split then split_evars oevd else [Int.Set.empty] in + let in_comp comp ev = if do_split then Int.Set.mem ev comp else true in let rec docomp evd = function | [] -> revert_resolvability oevd evd diff --git a/tactics/equality.ml b/tactics/equality.ml index ca54436a0..8d457d9f4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -878,7 +878,7 @@ let minimal_free_rels env sigma (c,cty) = let cty_rels = free_rels cty in let cty' = simpl env sigma cty in let rels' = free_rels cty' in - if Intset.subset cty_rels rels' then + if Int.Set.subset cty_rels rels' then (cty,cty_rels) else (cty',rels') @@ -888,10 +888,10 @@ let minimal_free_rels env sigma (c,cty) = let minimal_free_rels_rec env sigma = let rec minimalrec_free_rels_rec prev_rels (c,cty) = let (cty,direct_rels) = minimal_free_rels env sigma (c,cty) in - let combined_rels = Intset.union prev_rels direct_rels in + let combined_rels = Int.Set.union prev_rels direct_rels in let folder rels i = snd (minimalrec_free_rels_rec rels (c, type_of env sigma (mkRel i))) - in (cty, List.fold_left folder combined_rels (Intset.elements (Intset.diff direct_rels prev_rels))) - in minimalrec_free_rels_rec Intset.empty + in (cty, List.fold_left folder combined_rels (Int.Set.elements (Int.Set.diff direct_rels prev_rels))) + in minimalrec_free_rels_rec Int.Set.empty (* [sig_clausal_form siglen ty] @@ -1024,7 +1024,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let make_iterated_tuple env sigma dflt (z,zty) = let (zty,rels) = minimal_free_rels_rec env sigma (z,zty) in let sort_of_zty = get_sort_of env sigma zty in - let sorted_rels = Sort.list (<) (Intset.elements rels) in + let sorted_rels = Sort.list (<) (Int.Set.elements rels) in let (tuple,tuplety) = List.fold_left (make_tuple env sigma) (z,zty) sorted_rels in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a05ce2415..966309395 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2676,7 +2676,7 @@ let compute_elim_sig ?elimc elimt = let ccl = exchange_hd_app (mkVar (id_of_string "__QI_DUMMY__")) conclusion in let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in - let nparams = Intset.cardinal (free_rels concl_with_args) in + let nparams = Int.Set.cardinal (free_rels concl_with_args) in let preds,params = cut_list (List.length params_preds - nparams) params_preds in (* A first approximation, further analysis will tweak it *) |