Merge PR #7890: Inline a function from Quote used in setoid_ring.

3 files changed, 20 insertions, 25 deletions

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 e4d17f250..8e0ca877a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -96,34 +96,36 @@ let protect_tac_in map id =
 
 (****************************************************************************)
 
-let closed_term t l =
-  let open Quote_plugin in
+let rec closed_under sigma cset t =
+  try
+    let (gr, _) = Termops.global_of_constr sigma t in
+    Refset_env.mem gr cset
+  with Not_found ->
+    match EConstr.kind sigma t with
+    | Cast(c,_,_) -> closed_under sigma cset c
+    | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l
+    | _ -> false
+
+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 l = List.map UnivGen.constr_of_global l in
-  let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
-  if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
-
-(* TACTIC EXTEND echo
-| [ "echo" constr(t) ] ->
-  [ Pp.msg (Termops.print_constr t);  Tacinterp.eval_tactic (TacId []) ]
-END;;*)
+  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 =
-  TacFun([Some(Id.of_string"t")],
-  TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
-  [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t"));
-   Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l])))
-*)
-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 ->