diff options
| author | Maxime Dénès | 2017-05-05 18:12:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-05 18:12:55 +0200 |
| commit | e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 (patch) | |
| tree | db7cefecb217083cf3284c122ee4ce4c4a4eb56a | |
| parent | cd76a274c7d6fb71e109b6f3c87dd3a661f72e6c (diff) | |
Remove dead code and unused open.
| -rw-r--r-- | interp/implicit_quantifiers.ml | 6 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 5 |
2 files changed, 0 insertions, 11 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index d6749e918f..19c872b310 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -19,7 +19,6 @@ open Typeclasses_errors open Pp open Libobject open Nameops -open Misctypes open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -119,11 +118,6 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li | [] -> bdvars, l in aux bound l binders -let add_name_to_ids set na = - match na with - | Anonymous -> set - | Name id -> Id.Set.add id set - let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) = let rec vars bound vs = function | GVar (loc,id) -> 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 |