aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/proof_using.mli
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/proof_using.mli')
-rw-r--r--vernac/proof_using.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index ddab2742d..f63c8e242 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -14,8 +14,6 @@ val process_expr :
val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
-val to_string : Vernacexpr.section_subset_expr -> string
-
val suggest_constant : Environ.env -> Names.Constant.t -> unit
val suggest_variable : Environ.env -> Names.Id.t -> unit