From 8ad8fd120535eae0acc6f315b4ff1e8af81319dc Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 6 Oct 2013 20:44:38 +0000
Subject: Removing useless evar code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16854 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarutil.ml | 8 +++-----
 pretyping/evd.ml      | 4 ----
 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 :
-- 
cgit v1.2.3