Stop relying on side-effects for recursive scheme declaration.

Instead, we register functions dynamically declaring the dependencies of the
scheme to be generated.

We had to fix the test-suite because an internal scheme name changed.
We could also tweak the internal flag of scheme dependencies, but in this
particular case it looks more like a bug from the previous implementation.

7 files changed, 174 insertions, 94 deletions

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 910e042e7a..b08f4c8be7 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -62,7 +62,7 @@ let build_induction_scheme_in_type dep sort ind =
 
 let declare_individual_scheme_object name ?aux f =
   let f : individual_scheme_object_function =
-    fun _ ind -> f ind, Evd.empty_side_effects
+    fun _ ind -> f ind
   in
   declare_individual_scheme_object name ?aux f
 
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 98da61781e..000896bfea 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -229,7 +229,7 @@ let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
   (fun _ ind ->
     let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
-      (c, ctx), Evd.empty_side_effects)
+      (c, ctx))
 
 (**********************************************************************)
 (* Build the involutivity of symmetry for an inductive type           *)
@@ -248,17 +248,18 @@ let sym_scheme_kind =
 (**********************************************************************)
 
 let const_of_scheme kind env ind ctx =
-  let sym_scheme, eff = (find_scheme kind ind) in
+  let () = assert (check_scheme kind ind) in
+  let sym_scheme = lookup_scheme kind ind in
   let sym, ctx = with_context_set ctx
     (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in
-    mkConstU sym, ctx, eff
+    mkConstU sym, ctx
 
 let build_sym_involutive_scheme env ind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let eq,eqrefl,ctx = get_coq_eq ctx in
-  let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
+  let sym, ctx = const_of_scheme sym_scheme_kind env ind ctx in
   let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect mkRel n paramsctxt) in
   let inds = snd (mind_arity mip) in
   let indr = Sorts.relevance_of_sort_family inds in
@@ -297,10 +298,11 @@ let build_sym_involutive_scheme env ind =
                mkRel 1|])),
                mkRel 1 (* varH *),
                [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
-  in (c, UState.of_context_set ctx), eff
+  in (c, UState.of_context_set ctx)
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "_sym_involutive"
+  ~deps:(fun ind -> [SchemeIndividualDep (ind, sym_scheme_kind)])
   (fun _ ind ->
     build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
 
@@ -368,8 +370,8 @@ let build_l2r_rew_scheme dep env ind kind =
   let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
-  let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
-  let sym_involutive, ctx, eff' = const_of_scheme sym_involutive_scheme_kind env ind ctx in
+  let sym, ctx = const_of_scheme sym_scheme_kind env ind ctx in
+  let sym_involutive, ctx = const_of_scheme sym_involutive_scheme_kind env ind ctx in
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
@@ -454,8 +456,7 @@ let build_l2r_rew_scheme dep env ind kind =
        [|main_body|])
    else
      main_body))))))
-  in (c, UState.of_context_set ctx),
-      Evd.concat_side_effects eff' eff
+  in (c, UState.of_context_set ctx)
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -698,6 +699,10 @@ let build_r2l_rew_scheme dep env ind k =
 (**********************************************************************)
 let rew_l2r_dep_scheme_kind =
   declare_individual_scheme_object "_rew_r_dep"
+  ~deps:(fun ind -> [
+    SchemeIndividualDep (ind, sym_scheme_kind);
+    SchemeIndividualDep (ind, sym_involutive_scheme_kind);
+  ])
   (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
@@ -708,7 +713,7 @@ let rew_l2r_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_dep_scheme_kind =
   declare_individual_scheme_object "_rew_dep"
-  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
+  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -718,7 +723,7 @@ let rew_r2l_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_dep"
-  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
+  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -728,7 +733,7 @@ let rew_r2l_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
-  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects)
+  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -742,7 +747,7 @@ let rew_l2r_forward_dep_scheme_kind =
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
   (fun _ ind -> fix_r2l_forward_rew_scheme
-     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Evd.empty_side_effects)
+     (build_r2l_forward_rew_scheme false (Global.env()) ind InType))
 
 (**********************************************************************)
 (* Non-dependent rewrite from either right-to-left in conclusion or   *)
@@ -752,7 +757,7 @@ let rew_l2r_scheme_kind =
 (**********************************************************************)
 let rew_r2l_scheme_kind =
   declare_individual_scheme_object "_rew"
-  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Evd.empty_side_effects)
+  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType)
 
 (* End of rewriting schemes *)
 
@@ -835,5 +840,4 @@ let build_congr env (eq,refl,ctx) ind =
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
   (fun _ ind ->
      (* May fail if equality is not defined *)
-   build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind,
-   Evd.empty_side_effects)
+   build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index d1038f2655..6447708ace 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -27,7 +27,7 @@ val rew_r2l_scheme_kind : individual scheme_kind
 val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family ->
   constr Evd.in_evar_universe_context
 val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family ->
-  constr Evd.in_evar_universe_context * Evd.side_effects
+  constr Evd.in_evar_universe_context
 val build_r2l_forward_rew_scheme :
   bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context
 val build_l2r_forward_rew_scheme :
@@ -39,7 +39,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context
 val sym_scheme_kind : individual scheme_kind
 
 val build_sym_involutive_scheme : env -> inductive ->
-  constr Evd.in_evar_universe_context * Evd.side_effects
+  constr Evd.in_evar_universe_context
 val sym_involutive_scheme_kind : individual scheme_kind
 
 (** Builds a congruence scheme for an equality type *)
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e422366ed6..511cbb8b18 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -32,9 +32,9 @@ type internal_flag =
   | UserIndividualRequest   (* user action, a message is displayed *)
 
 type mutual_scheme_object_function =
-  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context
 
 type 'a scheme_kind = string
 
@@ -46,9 +46,13 @@ let pr_scheme_kind = Pp.str
 type individual
 type mutual
 
+type scheme_dependency =
+| SchemeMutualDep of MutInd.t * mutual scheme_kind
+| SchemeIndividualDep of inductive * individual scheme_kind
+
 type scheme_object_function =
-  | MutualSchemeFunction of mutual_scheme_object_function
-  | IndividualSchemeFunction of individual_scheme_object_function
+  | MutualSchemeFunction of mutual_scheme_object_function * (MutInd.t -> scheme_dependency list) option
+  | IndividualSchemeFunction of individual_scheme_object_function * (inductive -> scheme_dependency list) option
 
 let scheme_object_table =
   (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
@@ -68,11 +72,11 @@ let declare_scheme_object s aux f =
     Hashtbl.add scheme_object_table key (s,f);
     key
 
-let declare_mutual_scheme_object s ?(aux="") f =
-  declare_scheme_object s aux (MutualSchemeFunction f)
+let declare_mutual_scheme_object s ?deps ?(aux="") f =
+  declare_scheme_object s aux (MutualSchemeFunction (f, deps))
 
-let declare_individual_scheme_object s ?(aux="") f =
-  declare_scheme_object s aux (IndividualSchemeFunction f)
+let declare_individual_scheme_object s ?deps ?(aux="") f =
+  declare_scheme_object s aux (IndividualSchemeFunction (f, deps))
 
 (**********************************************************************)
 (* Defining/retrieving schemes *)
@@ -89,6 +93,10 @@ let compute_name internal id =
 let declare_definition_scheme = ref (fun ~internal ~univs ~role ~name c ->
     CErrors.anomaly (Pp.str "scheme declaration not registered"))
 
+let check_scheme kind ind =
+  try let _ = DeclareScheme.lookup_scheme kind ind in true
+  with Not_found -> false
+
 let define internal role id c poly univs =
   let id = compute_name internal id in
   let ctx = UState.minimize univs in
@@ -96,8 +104,9 @@ let define internal role id c poly univs =
   let univs = UState.univ_entry ~poly ctx in
   !declare_definition_scheme ~internal ~univs ~role ~name:id c
 
-let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
-  let (c, ctx), eff = f mode ind in
+(* Assumes that dependencies are already defined *)
+let rec define_individual_scheme_base kind suff f mode idopt (mind,i as ind) eff =
+  let (c, ctx) = f mode ind in
   let mib = Global.lookup_mind mind in
   let id = match idopt with
     | Some id -> id
@@ -105,17 +114,21 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let role = Evd.Schema (ind, kind) in
   let internal = mode == InternalTacticRequest in
   let const, neff = define internal role id c (Declareops.inductive_is_polymorphic mib) ctx in
+  let eff = Evd.concat_side_effects neff eff in
   DeclareScheme.declare_scheme kind [|ind,const|];
-  const, Evd.concat_side_effects neff eff
+  const, eff
 
-let define_individual_scheme kind mode names (mind,i as ind) =
+and define_individual_scheme kind mode names (mind,i as ind) =
   match Hashtbl.find scheme_object_table kind with
-  | _,MutualSchemeFunction f -> assert false
-  | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f mode names ind
-
-let define_mutual_scheme_base kind suff f mode names mind =
-  let (cl, ctx), eff = f mode mind in
+  | _,MutualSchemeFunction _ -> assert false
+  | 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 names ind eff
+
+(* Assumes that dependencies are already defined *)
+and define_mutual_scheme_base kind suff f mode names mind eff =
+  let (cl, ctx) = f mode mind in
   let mib = Global.lookup_mind mind in
   let ids = Array.init (Array.length mib.mind_packets) (fun i ->
       try Int.List.assoc i names
@@ -131,11 +144,25 @@ let define_mutual_scheme_base kind suff f mode names mind =
   DeclareScheme.declare_scheme kind schemes;
   consts, eff
 
-let define_mutual_scheme kind mode names mind =
+and define_mutual_scheme kind mode names mind =
   match Hashtbl.find scheme_object_table kind with
   | _,IndividualSchemeFunction _ -> assert false
-  | s,MutualSchemeFunction f ->
-      define_mutual_scheme_base kind s f mode names mind
+  | 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
+    define_mutual_scheme_base kind s f mode names mind eff
+
+and declare_scheme_dependence mode eff = function
+| SchemeIndividualDep (ind, kind) ->
+  if check_scheme kind ind then eff
+  else
+    let _, eff' = define_individual_scheme kind mode None ind in
+    Evd.concat_side_effects eff' eff
+| SchemeMutualDep (mind, kind) ->
+  if check_scheme kind (mind, 0) then eff
+  else
+    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
@@ -145,10 +172,14 @@ let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) =
   try find_scheme_on_env_too kind ind
   with Not_found ->
   match Hashtbl.find scheme_object_table kind with
-  | s,IndividualSchemeFunction f ->
-      define_individual_scheme_base kind s f mode None ind
-  | s,MutualSchemeFunction f ->
-      let ca, eff = define_mutual_scheme_base kind s f mode [] mind in
+  | 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
+  | 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
 
 let define_individual_scheme kind mode names ind =
@@ -157,8 +188,4 @@ let define_individual_scheme kind mode names ind =
 let define_mutual_scheme kind mode names mind =
   ignore (define_mutual_scheme kind mode names mind)
 
-let check_scheme kind ind =
-  try let _ = find_scheme_on_env_too kind ind in true
-  with Not_found -> false
-
 let lookup_scheme = DeclareScheme.lookup_scheme
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index 736de2af37..51f7ef9fd3 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -25,19 +25,27 @@ type internal_flag =
   | InternalTacticRequest
   | UserIndividualRequest
 
+type scheme_dependency =
+| SchemeMutualDep of MutInd.t * mutual scheme_kind
+| SchemeIndividualDep of inductive * individual scheme_kind
+
 type mutual_scheme_object_function =
-  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context
 type individual_scheme_object_function =
-  internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects
+  internal_flag -> inductive -> constr Evd.in_evar_universe_context
 
 (** Main functions to register a scheme builder. Note these functions
    are not safe to be used by plugins as their effects won't be undone
    on backtracking *)
 
-val declare_mutual_scheme_object : string -> ?aux:string ->
+val declare_mutual_scheme_object : string ->
+  ?deps:(MutInd.t -> scheme_dependency list) ->
+  ?aux:string ->
   mutual_scheme_object_function -> mutual scheme_kind
 
-val declare_individual_scheme_object : string -> ?aux:string ->
+val declare_individual_scheme_object : string ->
+  ?deps:(inductive -> scheme_dependency list) ->
+  ?aux:string ->
   individual_scheme_object_function ->
   individual scheme_kind
 
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
index 4b928007cf..273cb48295 100644
--- a/test-suite/success/Scheme.v
+++ b/test-suite/success/Scheme.v
@@ -18,7 +18,7 @@ Check myeq_rew.
 Check myeq_rew_dep.
 Check myeq_rew_fwd_dep.
 Check myeq_rew_r.
-Check internal_myeq_sym_involutive.
+Check myeq_sym_involutive.
 Check myeq_rew_r_dep.
 Check myeq_rew_fwd_r_dep.
 
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 215d5d97a0..b5f832d34d 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -122,6 +122,48 @@ let check_no_indices mib =
 
 let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
+let build_beq_scheme_deps kn =
+  (* fetching global env *)
+  let env = Global.env() in
+  (* fetching the mutual inductive body *)
+  let mib = Global.lookup_mind kn in
+  (* number of inductives in the mutual *)
+  let nb_ind = Array.length mib.mind_packets in
+  (* number of params in the type *)
+  let nparrec = mib.mind_nparams_rec in
+  check_no_indices mib;
+  let make_one_eq accu i =
+    let rec aux accu c =
+      let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
+      let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
+      match Constr.kind c with
+      | Cast (x,_,_) -> aux accu (Term.applist (x,a))
+      | App _ -> assert false
+      | Ind ((kn', _), _) ->
+          if MutInd.equal kn kn' then accu
+          else
+            let eff = SchemeMutualDep (kn', !beq_scheme_kind_aux ()) in
+            List.fold_left aux (eff :: accu) a
+      | Const (kn, u) ->
+        (match Environ.constant_opt_value_in env (kn, u) with
+        | Some c -> aux accu (Term.applist (c,a))
+        | None -> accu)
+      | Rel _ | Var _ | Sort _ | Prod _ | Lambda _ | LetIn _ | Proj _
+      | Construct _ | Case _ | CoFix _ | Fix _ | Meta _ | Evar _ | Int _
+      | Float _ -> accu
+    in
+    let u = Univ.Instance.empty in
+    let constrs n = get_constructors env (make_ind_family (((kn, i), u),
+      Context.Rel.to_extended_list mkRel (n+nb_ind-1) mib.mind_params_ctxt)) in
+    let constrsi = constrs (3+nparrec) in
+    let fold i accu arg =
+      let fold accu c = aux accu (RelDecl.get_type c) in
+      List.fold_left fold accu arg.cs_args
+    in
+    Array.fold_left_i fold accu constrsi
+  in
+  Array.fold_left_i (fun i accu _ -> make_one_eq accu i) [] mib.mind_packets
+
 let build_beq_scheme mode kn =
   check_bool_is_defined ();
   (* fetching global env *)
@@ -194,7 +236,7 @@ let build_beq_scheme mode kn =
         let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
         let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
         match Constr.kind c with
-        | Rel x -> mkRel (x-nlist+ndx), Evd.empty_side_effects
+        | Rel x -> mkRel (x-nlist+ndx)
         | Var x ->
           (* Support for working in a context with "eq_x : x -> x -> bool" *)
           let eid = Id.of_string ("eq_"^(Id.to_string x)) in
@@ -202,26 +244,22 @@ let build_beq_scheme mode kn =
             try ignore (Environ.lookup_named eid env)
             with Not_found -> raise (ParameterWithoutEquality (GlobRef.VarRef x))
           in
-          mkVar eid, Evd.empty_side_effects
+          mkVar eid
         | Cast (x,_,_) -> aux (Term.applist (x,a))
         | App _ -> assert false
         | Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
-            if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Evd.empty_side_effects
+            if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
             else begin
               try
-                let eq, eff =
-                  let c, eff = find_scheme ~mode (!beq_scheme_kind_aux()) (kn',i) in
-                  mkConst c, eff in
-                let eqa, eff =
-                  let eqa, effs = List.split (List.map aux a) in
-                  Array.of_list eqa,
-                  List.fold_left Evd.concat_side_effects eff (List.rev effs)
-                  in
+                let () = assert (check_scheme (!beq_scheme_kind_aux()) ind') in
+                let c = lookup_scheme (!beq_scheme_kind_aux()) ind' in
+                let eq = mkConst c in
+                let eqa = Array.of_list @@ List.map aux a in
                 let args =
                   Array.append
                     (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
-                if Int.equal (Array.length args) 0 then eq, eff
-                else mkApp (eq, args), eff
+                if Int.equal (Array.length args) 0 then eq
+                else mkApp (eq, args)
               with Not_found -> raise(EqNotFound (ind', fst ind))
             end
         | Sort _  -> raise InductiveWithSort
@@ -238,8 +276,7 @@ let build_beq_scheme mode kn =
                  let kneq = Constant.change_label kn eq_lbl in
                  if Environ.mem_constant kneq env then
                    let _ = Environ.constant_opt_value_in env (kneq, u) in
-                   Term.applist (mkConst kneq,a),
-                   Evd.empty_side_effects
+                   Term.applist (mkConst kneq,a)
                  else raise (ParameterWithoutEquality (GlobRef.ConstRef kn)))
         | Proj _ -> raise (EqUnknown "projection")
         | Construct _ -> raise (EqUnknown "constructor")
@@ -271,7 +308,6 @@ let build_beq_scheme mode kn =
     let constrsi = constrs (3+nparrec) in
     let n = Array.length constrsi in
     let ar = Array.make n (ff ()) in
-    let eff = ref Evd.empty_side_effects in
         for i=0 to n-1 do
           let nb_cstr_args = List.length constrsi.(i).cs_args in
           let ar2 = Array.make n (ff ()) in
@@ -283,13 +319,12 @@ let build_beq_scheme mode kn =
                     | _ -> let eqs = Array.make nb_cstr_args (tt ()) in
                       for ndx = 0 to nb_cstr_args-1 do
                         let cc = RelDecl.get_type (List.nth constrsi.(i).cs_args ndx) in
-                          let eqA, eff' = compute_A_equality rel_list
+                          let eqA = compute_A_equality rel_list
                                           nparrec
                                           (nparrec+3+2*nb_cstr_args)
                                           (nb_cstr_args+ndx+1)
                                           cc
                           in
-                          eff := Evd.concat_side_effects eff' !eff;
                           Array.set eqs ndx
                               (mkApp (eqA,
                                 [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
@@ -315,21 +350,18 @@ let build_beq_scheme mode kn =
         done;
         mkNamedLambda (make_annot (Id.of_string "X") Sorts.Relevant) (mkFullInd ind (nb_ind-1+1))  (
           mkNamedLambda (make_annot (Id.of_string "Y") Sorts.Relevant) (mkFullInd ind (nb_ind-1+2))  (
-            mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar))),
-        !eff
+            mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar)))
     in (* build_beq_scheme *)
     let names = Array.make nb_ind (make_annot Anonymous Sorts.Relevant) and
         types = Array.make nb_ind mkSet and
         cores = Array.make nb_ind mkSet in
-    let eff = ref Evd.empty_side_effects in
     let u = Univ.Instance.empty in
     for i=0 to (nb_ind-1) do
         names.(i) <- make_annot (Name (Id.of_string (rec_name i))) Sorts.Relevant;
         types.(i) <- mkArrow (mkFullInd ((kn,i),u) 0) Sorts.Relevant
                      (mkArrow (mkFullInd ((kn,i),u) 1) Sorts.Relevant (bb ()));
-        let c, eff' = make_one_eq i in
+        let c = make_one_eq i in
         cores.(i) <- c;
-        eff := Evd.concat_side_effects eff' !eff
     done;
       (Array.init nb_ind (fun i ->
       let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in
@@ -347,10 +379,12 @@ let build_beq_scheme mode kn =
           Vars.substl subst cores.(i)
         in
         create_input fix),
-       UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())),
-      !eff
+       UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()))
 
-let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
+let beq_scheme_kind =
+  declare_mutual_scheme_object "_beq"
+  ~deps:build_beq_scheme_deps
+  build_beq_scheme
 
 let _ = beq_scheme_kind_aux := fun () -> beq_scheme_kind
 
@@ -552,11 +586,11 @@ let eqI ind l =
   let list_id = list_id l in
   let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@
                            (List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
-  and e, eff =
-    try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
+  and e =
+    try let c = lookup_scheme beq_scheme_kind ind in mkConst c
     with Not_found -> user_err ~hdr:"AutoIndDecl.eqI"
       (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed.");
-  in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff
+  in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA))
 
 (**********************************************************************)
 (* Boolean->Leibniz *)
@@ -564,7 +598,7 @@ let eqI ind l =
 open Namegen
 
 let compute_bl_goal ind lnamesparrec nparrec =
-  let eqI, eff = eqI ind lnamesparrec in
+  let eqI = eqI ind lnamesparrec in
   let list_id = list_id lnamesparrec in
   let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
   let create_input c =
@@ -605,7 +639,7 @@ let compute_bl_goal ind lnamesparrec nparrec =
               (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|]))
               Sorts.Relevant
               (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
-        ))), eff
+        )))
 
 let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
@@ -695,16 +729,19 @@ let make_bl_scheme mode mind =
   let nparrec = mib.mind_nparams_rec in
   let lnonparrec,lnamesparrec = (* TODO subst *)
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
+  let bl_goal = compute_bl_goal ind lnamesparrec nparrec in
   let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
   let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
     (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec)
   in
-  ([|ans|], ctx), eff
+  ([|ans|], ctx)
 
-let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme
+let bl_scheme_kind =
+  declare_mutual_scheme_object "_dec_bl"
+  ~deps:(fun ind -> [SchemeMutualDep (ind, beq_scheme_kind)])
+  make_bl_scheme
 
 let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
 
@@ -715,7 +752,7 @@ let compute_lb_goal ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let eq = eq () and tt = tt () and bb = bb () in
   let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
-  let eqI, eff = eqI ind lnamesparrec in
+  let eqI = eqI ind lnamesparrec in
     let create_input c =
       let x = next_ident_away (Id.of_string "x") avoid and
           y = next_ident_away (Id.of_string "y") avoid in
@@ -755,7 +792,7 @@ let compute_lb_goal ind lnamesparrec nparrec =
               (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|]))
               Sorts.Relevant
               (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
-        ))), eff
+        )))
 
 let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
@@ -825,16 +862,19 @@ let make_lb_scheme mode mind =
   let nparrec = mib.mind_nparams_rec in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
-  let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
+  let lb_goal = compute_lb_goal ind lnamesparrec nparrec in
   let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let lb_goal = EConstr.of_constr lb_goal in
   let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
     (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
-  ([|ans|], ctx), eff
+  ([|ans|], ctx)
 
-let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
+let lb_scheme_kind =
+  declare_mutual_scheme_object "_dec_lb"
+  ~deps:(fun ind -> [SchemeMutualDep (ind, beq_scheme_kind)])
+  make_lb_scheme
 
 let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
 
@@ -909,7 +949,8 @@ 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 eqI, eff = eqI ind lnamesparrec in
+  let (_, eff) = find_scheme beq_scheme_kind ind in
+  let eqI = eqI ind lnamesparrec in
   let avoid = ref [] in
   let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
   let eqfalse x = mkApp(eq,[|bb;x;ff|]) in
@@ -1010,7 +1051,7 @@ let make_eq_decidability mode mind =
       ~typ:(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
       (compute_dec_tact ind lnamesparrec nparrec)
   in
-  ([|ans|], ctx), Evd.empty_side_effects
+  ([|ans|], ctx)
 
 let eq_dec_scheme_kind =
   declare_mutual_scheme_object "_eq_dec" make_eq_decidability