diff options
Diffstat (limited to 'plugins/setoid_ring/newring.ml')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b720b2e0a..2f6c00c9d 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) ] -> |