5 files changed, 28 insertions, 33 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 4c6156a38..4a691e442 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -130,8 +130,8 @@ type cinfo=
      ci_nhyps: int}     (* # projectable args *)
 
 let family_eq f1 f2 = match f1, f2 with
-  | Prop Pos, Prop Pos
-  | Prop Null, Prop Null
+  | Set, Set
+  | Prop, Prop
   | Type _, Type _ -> true
   | _ -> false
 
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index cc9c2046d..84baea964 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -199,11 +199,12 @@ let id_of_name = function
 	  let basename = Nametab.basename_of_global ref in
 	  basename
        | Sort s ->
-	  begin
+          begin
 	    match ESorts.kind sigma s with
-	    | Sorts.Prop _ -> Label.to_id (Label.make "Prop")
-	    | Sorts.Type _ -> Label.to_id (Label.make "Type")
-	  end
+            | Sorts.Prop -> Label.to_id (Label.make "Prop")
+            | Sorts.Set -> Label.to_id (Label.make "Set")
+            | Sorts.Type _ -> Label.to_id (Label.make "Type")
+          end
        | _ -> fail()
 
 
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 84b29a0bf..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,
@@ -148,8 +150,7 @@ let ic_unsafe c = (*FIXME remove *)
 
 let decl_constant na univs c =
   let open Constr in
-  let env = Global.env () in
-  let vars = Univops.universes_of_constr env c in
+  let vars = Univops.universes_of_constr c in
   let univs = Univops.restrict_universe_context univs vars in
   let univs = Monomorphic_const_entry univs in
   mkConst(declare_constant (Id.of_string na) 
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 ->