Merge PR #12202: Centralize the call to `tclEFFECTS` in scheme declaration

Reviewed-by: ejgallego

4 files changed, 29 insertions, 68 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8f2336c0e0..f3073acb0a 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -411,8 +411,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
   match EConstr.kind sigma hdcncl with
   | Ind (ind,u) ->
 
-      let c, eff = find_scheme scheme_name ind in
-      Proofview.tclEFFECTS eff <*>
+      find_scheme scheme_name ind >>= fun c ->
         pf_constr_of_global (GlobRef.ConstRef c)
   | _ -> assert false
   end
@@ -1001,14 +1000,13 @@ let ind_scheme_of_eq lbeq to_kind =
   let from_kind = inductive_sort_family mip in
   (* use ind rather than case by compatibility *)
   let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in
-  let c, eff = find_scheme kind (destIndRef lbeq.eq) in
-    GlobRef.ConstRef c, eff
+  find_scheme kind (destIndRef lbeq.eq) >>= fun c ->
+  Proofview.tclUNIT (GlobRef.ConstRef c)
 
 
 let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind =
   build_coq_I () >>= fun i ->
-  let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in
-  Proofview.tclEFFECTS eff <*>
+  ind_scheme_of_eq lbeq to_kind >>= fun eq_elim ->
     pf_constr_of_global eq_elim >>= fun eq_elim ->
     Proofview.tclUNIT
        (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]))
@@ -1352,10 +1350,10 @@ let inject_if_homogenous_dependent_pair ty =
     check_required_library ["Coq";"Logic";"Eqdep_dec"];
     let new_eq_args = [|pf_get_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in
     let inj2 = lib_ref "core.eqdep_dec.inj_pair2" in
-    let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
+    find_scheme (!eq_dec_scheme_kind_name()) ind >>= fun c ->
     (* cut with the good equality and prove the requested goal *)
     tclTHENLIST
-      [Proofview.tclEFFECTS eff;
+      [
        intro;
        onLastHyp (fun hyp ->
         Tacticals.New.pf_constr_of_global Coqlib.(lib_ref "core.eq.type") >>= fun ceq ->
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index ae27cf1019..9164a4ff26 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -165,23 +165,26 @@ and declare_scheme_dependence mode eff = function
     let _, eff' = define_mutual_scheme kind mode [] mind in
     Evd.concat_side_effects eff' eff
 
-let find_scheme_on_env_too kind ind =
-  let s = DeclareScheme.lookup_scheme kind ind in
-  s, Evd.empty_side_effects
-
 let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
-  try find_scheme_on_env_too kind ind
-  with Not_found ->
+  let open Proofview.Notations in
+  match lookup_scheme kind ind with
+  | Some s ->
+    (* FIXME: we need to perform this call to reset the environment, since the
+       imperative scheme table is desynchronized from the monadic interface. *)
+    Proofview.tclEFFECTS Evd.empty_side_effects <*>
+    Proofview.tclUNIT s
+  | None ->
   match Hashtbl.find scheme_object_table kind with
   | s,IndividualSchemeFunction (f, deps) ->
     let deps = match deps with None -> [] | Some deps -> deps ind in
     let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
-    define_individual_scheme_base kind s f mode None ind eff
+    let c, eff = define_individual_scheme_base kind s f mode None ind eff in
+    Proofview.tclEFFECTS eff <*> Proofview.tclUNIT c
   | s,MutualSchemeFunction (f, deps) ->
     let deps = match deps with None -> [] | Some deps -> deps mind in
     let eff = List.fold_left (fun eff dep -> declare_scheme_dependence mode eff dep) Evd.empty_side_effects deps in
     let ca, eff = define_mutual_scheme_base kind s f mode [] mind eff in
-      ca.(i), eff
+    Proofview.tclEFFECTS eff <*> Proofview.tclUNIT ca.(i)
 
 let define_individual_scheme kind mode names ind =
   ignore (define_individual_scheme kind mode names ind)
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 9259a4a540..09fb051194 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -59,7 +59,7 @@ val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -
   (int * Id.t) list -> MutInd.t -> unit
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t Proofview.tactic
 
 (** Like [find_scheme] but does not generate a constant on the fly *)
 val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t option
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index bfa7a729f7..ebea5e146c 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -441,24 +441,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
     let type_of_pq = Tacmach.New.pf_get_type_of gl p in
     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 lb_type_of_p =
-        try
-          let c, eff = find_scheme ~mode lb_scheme_key (fst u) (*FIXME*) in
-          Proofview.tclUNIT (mkConst c, eff)
-        with Not_found ->
-          (* spiwack: the format of this error message should probably
-                      be improved. *)
-          let err_msg =
-            (str "Leibniz->boolean:" ++
-             str "You have to declare the" ++
-             str "decidability over " ++
-             Printer.pr_econstr_env env sigma type_of_pq ++
-             str " first.")
-          in
-          Tacticals.New.tclZEROMSG err_msg
-       in
-       lb_type_of_p >>= fun (lb_type_of_p,eff) ->
+    let u,v = destruct_ind env sigma type_of_pq 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
                           v
@@ -468,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
 
@@ -514,22 +498,9 @@ 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 bl_t1, eff =
-               try
-                 let c, eff = find_scheme bl_scheme_key (fst u) (*FIXME*) in
-                 mkConst c, eff
-               with Not_found ->
-                 (* spiwack: the format of this error message should probably
-                             be improved. *)
-                 let err_msg =
-                                        (str "boolean->Leibniz:" ++
-                                         str "You have to declare the" ++
-                                         str "decidability over " ++
-                                         Printer.pr_econstr_env env sigma tt1 ++
-                                         str " first.")
-                 in
-                 user_err err_msg
-               in let bl_args =
+               find_scheme bl_scheme_key (fst u) (*FIXME*) >>= fun c ->
+               let bl_t1 = mkConst c in
+               let bl_args =
                         Array.append (Array.append
                           v
                           (Array.Smart.map (fun x -> do_arg env sigma u x 1) v))
@@ -539,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 ]
@@ -956,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
@@ -979,21 +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
-  begin try
-          let c, eff = find_scheme bl_scheme_kind ind in
-          Proofview.tclUNIT (mkConst c,eff) with
-    Not_found ->
-      Tacticals.New.tclZEROMSG (str "Error during the decidability part, boolean to leibniz equality is required.")
-  end >>= fun (blI,eff') ->
-  begin try
-          let c, eff = find_scheme lb_scheme_kind ind in
-          Proofview.tclUNIT (mkConst c,eff) with
-    Not_found ->
-      Tacticals.New.tclZEROMSG (str "Error during the decidability part, leibniz to boolean equality is required.")
-  end >>= fun (lbI,eff'') ->
-  let eff = (Evd.concat_side_effects eff'' (Evd.concat_side_effects eff' eff)) in
+  find_scheme bl_scheme_kind ind >>= fun c ->
+  let blI = mkConst c in
+  find_scheme lb_scheme_kind ind >>= fun c ->
+  let lbI = mkConst c 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 *)