diff options
| author | Pierre-Marie Pédrot | 2018-10-03 14:48:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-03 14:48:43 +0200 |
| commit | 920cc6ba6ee33bf34cd853f6a9a050ed7594e2ce (patch) | |
| tree | c3874e606bdbac3bf6c3f093587e5dda8dae37ec /pretyping/typeclasses.ml | |
| parent | 016f4a302090bcbb4ad47197dda2c60d6f598f6a (diff) | |
| parent | e5b3bd6b12af9f08d7913e25748fba9c4f9fd48f (diff) | |
Merge PR #8596: [api] Cleanup `Decls`: remove unused function, move vernac helper.
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 55d9838bbb..67c5643459 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -11,7 +11,6 @@ (*i*) open Names open Globnames -open Decl_kinds open Term open Constr open Vars @@ -482,19 +481,6 @@ let instances r = let is_class gr = GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes -let is_instance = function - | ConstRef c -> - (match Decls.constant_kind c with - | IsDefinition Instance -> true - | _ -> false) - | VarRef v -> - (match Decls.variable_kind v with - | IsDefinition Instance -> true - | _ -> false) - | ConstructRef (ind,_) -> - is_class (IndRef ind) - | _ -> false - (* To embed a boolean for resolvability status. This is essentially a hack to mark which evars correspond to goals and do not need to be resolved when we have nested [resolve_all_evars] |