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.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'plugins/setoid_ring/newring.ml') 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, -- cgit v1.2.3