diff options
| author | ppedrot | 2013-10-06 20:44:38 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-06 20:44:38 +0000 |
| commit | 8ad8fd120535eae0acc6f315b4ff1e8af81319dc (patch) | |
| tree | adf9ad422d78e3b36b9263feec1a652e383c0a5c | |
| parent | fd4bb20be1cdde645391ad514db8525c14d2a05e (diff) | |
Removing useless evar code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16854 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evarutil.ml | 8 | ||||
| -rw-r--r-- | pretyping/evd.ml | 4 | ||||
| -rw-r--r-- | pretyping/evd.mli | 4 |
3 files changed, 3 insertions, 13 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f66e5f7083..dec5e811ca 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -80,14 +80,12 @@ let nf_evar_info evc info = | Evar_empty -> Evar_empty | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) } -let nf_evars evm = Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm +let nf_evar_map evm = + Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm -let nf_evars_undefined evm = +let nf_evar_map_undefined evm = Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) evm -let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd -let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd - (*-------------------*) (* Auxiliary functions for the conversion algorithms modulo evars *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 28ab4f1a5b..df02975ce5 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -244,12 +244,8 @@ let to_list d = let undefined_map d = d.undf_evars -let defined_map d = d.defn_evars - let undefined_evars d = { d with defn_evars = EvMap.empty } -let defined_evars d = { d with undf_evars = EvMap.empty } - (* spiwack: not clear what folding over an evar_map, for now we shall simply fold over the inner evar_map. *) let fold f d a = diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 554ce1bf2a..12699309b5 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -152,9 +152,6 @@ val add_constraints : evar_map -> Univ.constraints -> evar_map val undefined_map : evar_map -> evar_info Evar.Map.t (** Access the undefined evar mapping directly. *) -val defined_map : evar_map -> evar_info Evar.Map.t -(** Access the defined evar mapping directly. *) - (** {6 Instantiating partial terms} *) exception NotInstantiatedEvar @@ -180,7 +177,6 @@ val evars_reset_evd : ?with_conv_pbs:bool -> evar_map -> evar_map -> evar_map (** {6 Misc} *) val undefined_evars : evar_map -> evar_map -val defined_evars : evar_map -> evar_map (** TODO: see where we can replace those functions by their [_map] variant. *) val evar_declare : |