diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 4 insertions, 6 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 71312259ed..63d77af662 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -509,9 +509,8 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) = context at globalization time: we retype with the now known intros/lettac/inversion hypothesis names *) | Some c -> - let fold id _ accu = Id.Set.add id accu in - let ltacvars = Id.Map.fold fold constrvars Id.Set.empty in - let bndvars = Id.Map.fold fold ist.lfun Id.Set.empty in + let ltacvars = Id.Map.domain constrvars in + let bndvars = Id.Map.domain ist.lfun in let ltacdata = (ltacvars, bndvars) in intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c in @@ -1961,8 +1960,7 @@ let interp_tac_gen lfun avoid_ids debug t gl = let extra = TacStore.set TacStore.empty f_debug debug in let extra = TacStore.set extra f_avoid_ids avoid_ids in let ist = { lfun = lfun; extra = extra } in - let fold x _ accu = Id.Set.add x accu in - let ltacvars = Id.Map.fold fold lfun Id.Set.empty in + let ltacvars = Id.Map.domain lfun in interp_tactic ist (intern_pure_tactic { ltacvars; ltacrecvars = Id.Map.empty; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b0f150158d..a6826b9db9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2447,7 +2447,7 @@ let hyps_of_vars env sign nogen hyps = else if Id.Set.mem x hs then (hs,x::hl) else let xvars = global_vars_set_of_decl env d in - if not (Id.Set.equal (Id.Set.diff xvars hs) Id.Set.empty) then + if not (Id.Set.is_empty (Id.Set.diff xvars hs)) then (Id.Set.add x hs, x :: hl) else (hs, hl)) ~init:(hyps,[]) |