aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml43
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 30ceb10182..74ad34eff6 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -179,8 +179,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 Evd.Store.empty in
- {Evd.it = gl; Evd.eff=Declareops.no_seff;
- Evd.sigma = sigma}
+ {Evd.it = gl; Evd.sigma = sigma}
let exec_tactic env n f args =
let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in