2 files changed, 6 insertions, 7 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index cca17a17e1..e18df6e460 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -51,13 +51,13 @@ let _ =
 
 let tcl_change_info_gen info_gen =
   (fun gls ->
-     let it, eff = sig_it gls, sig_eff gls in
+     let it = sig_it gls in
      let concl = pf_concl gls in
      let hyps = Goal.V82.hyps (project gls) it in
      let extra = Goal.V82.extra (project gls) it in
      let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
      let sigma = Goal.V82.partial_solution sigma it ev in
-     { it = [gl] ; sigma= sigma; eff = eff } )
+     { it = [gl] ; sigma= sigma; } )
 
 let tcl_change_info info gls =
   let info_gen s = Store.set s Decl_mode.info info in
@@ -129,7 +129,7 @@ let go_to_proof_mode () =
 
 let daimon_tac gls =
   set_daimon_flag ();
-  {it=[];sigma=sig_sig gls;eff=gls.eff}
+  {it=[];sigma=sig_sig gls;}
 
 (* post-instruction focus management *)
 
@@ -1455,8 +1455,8 @@ let do_instr raw_instr pts =
   let has_tactic = preprocess pts raw_instr.instr in
   begin
     if has_tactic then
-            let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in
-      let gl = { it=List.hd gls ; sigma=sigma; eff=eff } in
+            let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
+      let gl = { it=List.hd gls ; sigma=sigma; } in
       let env=  pf_env gl in
       let ist = {ltacvars = Id.Set.empty; ltacrecvars = Id.Map.empty;
 		 gsigma = sigma; genv = env} in
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