aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 35189f786b..a0f565ce36 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -174,7 +174,7 @@ let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
let dummy_goal env =
let (gl,_,sigma) =
- Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Store.empty in
+ Goal.V82.mk_goal Evd.empty (named_context_val env) mkProp Evd.Store.empty in
{Evd.it = gl;
Evd.sigma = sigma}