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.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 57312cb4b..090671e04 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -23,4 +23,4 @@ val w_refine : env -> evar -> Rawterm.rawconstr -> evar_defs -> evar_defs
val instantiate_pf_com :
int -> Topconstr.constr_expr -> pftreestate -> pftreestate
-(* the instantiate tactic was moved to tactics/evar_tactics.ml *)
+(* the instantiate tactic was moved to [tactics/evar_tactics.ml] *)