Merge the call to tclEFFECTS into find_scheme.

This encapsulates better the invariants of this function.

1 files changed, 5 insertions, 9 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 5fb12092d7..ebea5e146c 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -442,7 +442,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
     let sigma = Tacmach.New.project gl in
     let env = Tacmach.New.pf_env gl in
     let u,v = destruct_ind env sigma type_of_pq in
-    let c, eff = find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) in
+    find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) >>= fun c ->
     let lb_type_of_p = mkConst c in
        Proofview.tclEVARMAP >>= fun sigma ->
        let lb_args = Array.append (Array.append
@@ -453,7 +453,6 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
                        then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
            in
            Tacticals.New.tclTHENLIST [
-             Proofview.tclEFFECTS eff;
              Equality.replace p q ; apply app ; Auto.default_auto]
   end
 
@@ -499,7 +498,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
           in if eq_ind (fst u) ind
              then Tacticals.New.tclTHENLIST [Equality.replace t1 t2; Auto.default_auto ; aux q1 q2 ]
              else (
-               let c, eff = find_scheme bl_scheme_key (fst u) (*FIXME*) in
+               find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c ->
                let bl_t1 = mkConst c in
                let bl_args =
                         Array.append (Array.append
@@ -511,7 +510,6 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                            then bl_t1 else mkApp (bl_t1,bl_args)
                 in
                 Tacticals.New.tclTHENLIST [
-                  Proofview.tclEFFECTS eff;
                   Equality.replace_by t1 t2
                     (Tacticals.New.tclTHEN (apply app) (Auto.default_auto)) ;
                   aux q1 q2 ]
@@ -928,7 +926,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
   let eq = eq () and tt = tt ()
   and ff = ff () and bb = bb () in
   let list_id = list_id lnamesparrec in
-  let (_, eff) = find_scheme beq_scheme_kind ind in
+  find_scheme beq_scheme_kind ind >>= fun _ ->
   let eqI = eqI ind lnamesparrec in
   let avoid = ref [] in
   let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
@@ -951,13 +949,11 @@ let compute_dec_tact ind lnamesparrec nparrec =
   let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
   let arfresh = Array.of_list fresh_first_intros in
   let xargs = Array.sub arfresh 0 (2*nparrec) in
-  let c, eff' = find_scheme bl_scheme_kind ind in
+  find_scheme bl_scheme_kind ind >>= fun c ->
   let blI = mkConst c in
-  let c, eff'' = find_scheme lb_scheme_kind ind in
+  find_scheme lb_scheme_kind ind >>= fun c ->
   let lbI = mkConst c in
-  let eff = (Evd.concat_side_effects eff'' (Evd.concat_side_effects eff' eff)) in
   Tacticals.New.tclTHENLIST [
-        Proofview.tclEFFECTS eff;
         intros_using fresh_first_intros;
         intros_using [freshn;freshm];
         (*we do this so we don't have to prove the same goal twice *)