diff options
| author | Pierre-Marie Pédrot | 2013-11-30 01:42:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2013-11-30 01:42:45 +0100 |
| commit | 2b2cb750e396f1a2e9cd96371ac7034ba34349e4 (patch) | |
| tree | ba2257adc0d915cbc7718d581c620ba371033cbb | |
| parent | b9b737fee66e954c70bbedbe67517e5b91cc0efb (diff) | |
Useless instantiation function exported in Evd.
| -rw-r--r-- | pretyping/evd.ml | 15 | ||||
| -rw-r--r-- | pretyping/evd.mli | 1 |
2 files changed, 0 insertions, 16 deletions
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 |