Removing useless meta-related functions.

4 files changed, 0 insertions, 38 deletions

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} *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 4f2dd2f337..54e7fbf914 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -32,8 +32,6 @@ let trace s =
 let succfix (depth, fixrels) =
   (succ depth, List.map succ fixrels)
 
-let mkMetas n = List.init n (fun _ -> Evarutil.mk_new_meta ())
-
 let check_evars env evm =
   Evar.Map.iter
   (fun key evi ->
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index feebf94ec4..04292422cc 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -31,8 +31,6 @@ val declare_definition_ref :
 
 val check_evars : env -> evar_map -> unit
 
-val mkMetas : int -> constr list
-
 val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t
 val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list