From 2b2cb750e396f1a2e9cd96371ac7034ba34349e4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 30 Nov 2013 01:42:45 +0100
Subject: Useless instantiation function exported in Evd.

---
 pretyping/evd.ml  | 15 ---------------
 pretyping/evd.mli |  1 -
 2 files changed, 16 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5537d87d03..5870a22b73 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -222,15 +222,6 @@ let eq_evar_info ei1 ei2 =
 exception NotInstantiatedEvar
 
 (* Note: let-in contributes to the instance *)
-let make_evar_instance sign args =
-  let rec instrec sign args = match sign, args with
-  | [], [] -> []
-  | (id,_,_) :: sign, c :: args ->
-    if isVarId id c then instrec sign args
-    else (id, c) :: instrec sign args
-  | [], _ | _, [] -> instance_mismatch ()
-  in
-  instrec sign args
 
 let make_evar_instance_array info args =
   let len = Array.length args in
@@ -251,12 +242,6 @@ let make_evar_instance_array info args =
   let filter = Filter.repr (evar_filter info) in
   instrec filter (evar_context info) 0
 
-let instantiate_evar sign c args =
-  let inst = make_evar_instance sign args in
-  match inst with
-  | [] -> c
-  | _ -> replace_vars inst c
-
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
   match inst with
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ec16f53b76..58e4cd630b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -218,7 +218,6 @@ val existential_opt_value : evar_map -> existential -> constr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
-val instantiate_evar : named_context -> constr -> constr list -> constr
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
 
 val subst_evar_defs_light : substitution -> evar_map -> evar_map
-- 
cgit v1.2.3