diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-21 11:09:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-21 12:16:07 +0200 |
| commit | 890111168d80e6217c73bedda2f1381fa76524be (patch) | |
| tree | fd160df67f883eb8365557ca8ba2c0ee73172bf0 /pretyping/evd.ml | |
| parent | be0121602ff9fb3200cafead25e325617164038a (diff) | |
Dead code.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index b8886b9b5..a41db3f8f 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -934,18 +934,6 @@ let loc_of_conv_pb evd (pbty,env,t1,t2) = (** The following functions return the set of evars immediately contained in the object *) -(* including defined evars, excluding instances *) - -let collect_evars c = - let rec collrec acc c = - match kind_of_term c with - | Evar (evk,_) -> Evar.Set.add evk acc - | _ -> fold_constr collrec acc c - in - collrec Evar.Set.empty c - -(* including defined evars and instances of evars *) - (* excluding defined evars *) let evar_list c = |