Merge the call to tclEFFECTS into find_scheme.

This encapsulates better the invariants of this function.

3 files changed, 18 insertions, 17 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