From 32f6c4ee62146810c72cb5c86f341c8ca77be909 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 3 Dec 2013 18:40:56 +0100
Subject: Removing useless meta-related functions.

---
 pretyping/evarutil.ml  | 29 -----------------------------
 pretyping/evarutil.mli |  5 -----
 2 files changed, 34 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 780da888e2..7378467661 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -212,35 +212,6 @@ let push_duplicated_evars sigma emap c =
   in
   snd (collrec ([],(sigma,emap)) c)
 
-(* replaces a mapping of existentials into a mapping of metas.
-   Problem if an evar appears in the type of another one (pops anomaly) *)
-let evars_to_metas sigma (emap, c) =
-  let emap = nf_evar_map_undefined emap in
-  let sigma',emap' = push_dependent_evars sigma emap in
-  let sigma',emap' = push_duplicated_evars sigma' emap' c in
-  (* if an evar has been instantiated in [emap] (as part of typing [c])
-     then it is instantiated in [sigma]. *)
-  let repair_evars sigma emap =
-    fold_undefined begin fun ev _ sigma' ->
-      try
-	let info = find emap ev in
-	match evar_body info with
-	| Evar_empty -> sigma'
-	| Evar_defined body -> define ev body sigma'
-      with Not_found -> sigma'
-    end sigma sigma
-  in
-  let sigma' = repair_evars sigma' emap in
-  let change_exist evar =
-    let ty = nf_betaiota emap (existential_type emap evar) in
-    let n = new_meta() in
-    mkCast (mkMeta n, DEFAULTcast, ty) in
-  let rec replace c =
-    match kind_of_term c with
-      | Evar (evk,_ as ev) when Evd.mem emap' evk -> change_exist ev
-      | _ -> map_constr replace c in
-  (sigma', replace c)
-
 (* The list of non-instantiated existential declarations (order is important) *)
 
 let non_instantiated sigma =
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 05d994f0a6..7e1f7df88b 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -58,11 +58,6 @@ val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
 
 (** {6 Evars/Metas switching...} *)
 
-(** [evars_to_metas] generates new metavariables for each non dependent
-   existential and performs the replacement in the given constr; it also
-   returns the evar_map extended with dependent evars *)
-val evars_to_metas : evar_map -> open_constr -> (evar_map * constr)
-
 val non_instantiated : evar_map -> evar_info Evar.Map.t
 
 (** {6 Unification utils} *)
-- 
cgit v1.2.3