diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/glob_ops.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 080ec5ed12..6509aaac3d 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -266,11 +266,6 @@ let occur_glob_constr id = fold_glob_constr_with_binders g f barred acc c in occur false false -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Id.Set.add id set - let free_glob_vars = let rec vars bound vs = function | GVar (loc,id') -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs |