From 315aa093490d533e3d8db7a24bde78ed812c3b0d Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 21 Jun 2018 17:45:27 +0200 Subject: Further cleanup: do not export the closed_term Ltac entry. We only use it locally, so we simply register the ML tactic inside the module but we do not export the syntax. --- plugins/setoid_ring/newring.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'plugins/setoid_ring/newring.mli') diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index 0e056a472..fcd04a2e7 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -18,8 +18,6 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic val protect_tac : string -> unit Proofview.tactic -val closed_term : EConstr.constr -> GlobRef.t list -> unit Proofview.tactic - val add_theory : Id.t -> constr_expr -> -- cgit v1.2.3