aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/evar_refiner.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/evar_refiner.mli')
-rw-r--r--proofs/evar_refiner.mli5
1 files changed, 0 insertions, 5 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 35a3e5d82..e3778e94c 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -13,8 +13,3 @@ open Pretyping
val w_refine : evar * evar_info ->
glob_constr_ltac_closure -> evar_map -> evar_map
-
-val instantiate_pf_com :
- Evd.evar -> Constrexpr.constr_expr -> Evd.evar_map -> Evd.evar_map
-
-(** the instantiate tactic was moved to [tactics/evar_tactics.ml] *)