From 74826c1869a423b4e7224d3f69180584bdef1726 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 27 Sep 2017 16:54:41 +0200 Subject: Parse [Proof using Type] without translating Type to an id. --- vernac/proof_using.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'vernac/proof_using.mli') 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 -- cgit v1.2.3