aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/evar_refiner.ml')
-rw-r--r--proofs/evar_refiner.ml11
1 files changed, 0 insertions, 11 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 059ae54c9..3192a6a29 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -59,14 +59,3 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
str (string_of_existential evk))
in
define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma)
-
-(* vernac command Existential *)
-
-(* Main component of vernac command Existential *)
-let instantiate_pf_com evk com sigma =
- let evi = Evd.find sigma evk in
- let env = Evd.evar_filtered_env evi in
- let rawc = Constrintern.intern_constr env com in
- let ltac_vars = Pretyping.empty_lvar in
- let sigma' = w_refine (evk, evi) (ltac_vars, rawc) sigma in
- sigma'