From a327ae04966aa1c7786ae32157516e934068ea89 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Nov 2016 21:33:14 +0100
Subject: Quote API using EConstr.

---
 plugins/setoid_ring/g_newring.ml4 | 2 +-
 plugins/setoid_ring/newring.ml    | 3 ++-
 plugins/setoid_ring/newring.mli   | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins/setoid_ring')

diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 0987c44ae2..89ec4c1c52 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -30,7 +30,7 @@ END
 
 TACTIC EXTEND closed_term
   [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] ->
-    [ closed_term t l ]
+    [ closed_term (EConstr.of_constr t) l ]
 END
 
 open Pptactic
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b720b2e0a8..2f6c00c9d6 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -97,9 +97,10 @@ let protect_tac_in map id =
 
 let closed_term t l =
   let open Quote_plugin in
+  Proofview.tclEVARMAP >>= fun sigma ->
   let l = List.map Universes.constr_of_global l in
   let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in
-  if Quote.closed_under cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
+  if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt())
 
 (* TACTIC EXTEND echo
 | [ "echo" constr(t) ] ->
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index f417c87cde..89538eb24c 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -19,7 +19,7 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic
 
 val protect_tac : string -> unit Proofview.tactic
 
-val closed_term : constr -> global_reference list -> unit Proofview.tactic
+val closed_term : EConstr.constr -> global_reference list -> unit Proofview.tactic
 
 val process_ring_mods :
   constr_expr ring_mod list ->
-- 
cgit v1.2.3