diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-03 17:57:16 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-05-03 17:57:16 +0000 |
| commit | a35a77559f93141a6493f437405370f725ae2fbb (patch) | |
| tree | ffd3a2dc5a5b0213a045bd71d6004f1feffeec31 | |
| 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
| -rw-r--r-- | pretyping/evd.ml | 2 | ||||
| -rw-r--r-- | pretyping/evd.mli | 2 | ||||
| -rw-r--r-- | proofs/clenv.ml | 4 |
3 files changed, 2 insertions, 6 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 28b6ac93b..cc525dca1 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 52c24a3f2..49878ce8a 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 } diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 156629c19..bc6da8c34 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -157,7 +157,7 @@ let mentions clenv mv0 = | Some (b,_) -> b.freemetas | None -> Metaset.empty with Not_found -> Metaset.empty in - meta_exists menrec mlist + Metaset.exists menrec mlist in menrec let error_incompatible_inst clenv mv = @@ -173,7 +173,7 @@ let error_incompatible_inst clenv mv = (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) let clenv_assign mv rhs clenv = let rhs_fls = mk_freelisted rhs in - if meta_exists (mentions clenv mv) rhs_fls.freemetas then + if Metaset.exists (mentions clenv mv) rhs_fls.freemetas then error "clenv_assign: circularity in unification"; try if meta_defined clenv.evd mv then |