diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 17:33:26 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 18:12:25 +0100 |
| commit | 48e4831fa56e3b0acd92aabdb78847696b84daf7 (patch) | |
| tree | 678867d85a8201ddd7138dcb7295c2d71170eb01 /proofs/evar_refiner.ml | |
| parent | 2349d740caa4d9248ba5485aebbcce9ec18d3fd2 (diff) | |
Extruding the code for the Existential command from Proofview.
Diffstat (limited to 'proofs/evar_refiner.ml')
| -rw-r--r-- | proofs/evar_refiner.ml | 11 |
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' |