From 315aa093490d533e3d8db7a24bde78ed812c3b0d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
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/g_newring.ml4 |  5 -----
 plugins/setoid_ring/newring.ml    | 10 ++++++++--
 plugins/setoid_ring/newring.mli   |  2 --
 3 files changed, 8 insertions(+), 9 deletions(-)

(limited to 'plugins')

diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index e9ce306e8..4ea0b30bd 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -29,11 +29,6 @@ TACTIC EXTEND protect_fv
     [ protect_tac map ]
 END
 
-TACTIC EXTEND closed_term
-  [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
-    [ closed_term t l ]
-END
-
 open Pptactic
 open Ppconstr
 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index eabe2e13f..9e9553753 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -106,20 +106,26 @@ let rec closed_under sigma cset t =
     | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l
     | _ -> false
 
-let closed_term t l =
+let closed_term args _ = match args with
+| [t; l] ->
+  let t = Option.get (Value.to_constr t) in
+  let l = List.map (fun c -> Value.cast (Genarg.topwit Stdarg.wit_ref) c) (Option.get (Value.to_list l)) in
   Proofview.tclEVARMAP >>= fun sigma ->
   let cs = List.fold_right Refset_env.add l Refset_env.empty in
   if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
+| _ -> assert false
 
-let closed_term_ast l =
+let closed_term_ast =
   let tacname = {
     mltac_plugin = "newring_plugin";
     mltac_tactic = "closed_term";
   } in
+  let () = Tacenv.register_ml_tactic tacname [|closed_term|] in
   let tacname = {
     mltac_name = tacname;
     mltac_index = 0;
   } in
+  fun l ->
   let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
   TacFun([Name(Id.of_string"t")],
   TacML(Loc.tag (tacname,
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