From 48e4831fa56e3b0acd92aabdb78847696b84daf7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 17:33:26 +0100 Subject: Extruding the code for the Existential command from Proofview. --- proofs/evar_refiner.ml | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'proofs/evar_refiner.ml') 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' -- cgit v1.2.3