diff options
| author | ppedrot | 2013-05-03 17:57:16 +0000 |
|---|---|---|
| committer | ppedrot | 2013-05-03 17:57:16 +0000 |
| commit | a35a77559f93141a6493f437405370f725ae2fbb (patch) | |
| tree | ffd3a2dc5a5b0213a045bd71d6004f1feffeec31 /pretyping | |
| parent | bddb6d173c4c3c570737ba74ad3dfa610d304157 (diff) | |
Removing a redundant function from Evd.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16465 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 28b6ac93b5..cc525dca1e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -317,8 +317,6 @@ let clb_name = function module Metaset = Int.Set -let meta_exists p s = Metaset.fold (fun x b -> b || (p x)) s false - module Metamap = Int.Map let metamap_to_list m = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 52c24a3f20..49878ce8aa 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -23,8 +23,6 @@ module Metamap : Map.S with type key = metavariable module Metaset : Set.S with type elt = metavariable -val meta_exists : (metavariable -> bool) -> Metaset.t -> bool - type 'a freelisted = { rebus : 'a; freemetas : Metaset.t } |