Imported Upstream version 8.5~beta3+dfsg

1 files changed, 14 insertions, 13 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 8643fe10..b2603315 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -191,9 +191,9 @@ let build_sym_scheme env ind =
 
 let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
-  (fun ind -> 
+  (fun _ ind ->
     let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
-      (c, ctx), Declareops.no_seff)
+      (c, ctx), Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Build the involutivity of symmetry for an inductive type           *)
@@ -262,7 +262,7 @@ let build_sym_involutive_scheme env ind =
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "_sym_involutive"
-  (fun ind -> 
+  (fun _ ind ->
     build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
 
 (**********************************************************************)
@@ -412,7 +412,8 @@ let build_l2r_rew_scheme dep env ind kind =
        [|main_body|])
    else
      main_body))))))
-  in (c, Evd.evar_universe_context_of ctx), Declareops.union_side_effects eff' eff
+  in (c, Evd.evar_universe_context_of ctx),
+      Safe_typing.concat_private eff' eff
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -650,7 +651,7 @@ let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme
 (**********************************************************************)
 let rew_l2r_dep_scheme_kind =
   declare_individual_scheme_object "_rew_r_dep"
-  (fun ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
+  (fun _ ind -> build_l2r_rew_scheme true (Global.env()) ind InType)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in conclusion                 *)
@@ -660,7 +661,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,Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -670,7 +671,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,Declareops.no_seff)
+  (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -680,7 +681,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,Declareops.no_seff)
+  (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -693,8 +694,8 @@ 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), Declareops.no_seff)
+  (fun _ ind -> fix_r2l_forward_rew_scheme
+     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either right-to-left in conclusion or   *)
@@ -704,7 +705,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, Declareops.no_seff)
+  (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants)
 
 (* End of rewriting schemes *)
 
@@ -780,6 +781,6 @@ let build_congr env (eq,refl,ctx) ind =
   in c, Evd.evar_universe_context_of ctx
 
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
-  (fun ind ->
+  (fun _ ind ->
     (* May fail if equality is not defined *)
-    build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff)
+    build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants)