Avoid type checking private_constants (side_eff) again during Qed (#4357).

Side effects are now an opaque data type, called private_constant, you can
only obtain from safe_typing.  When add_constant is called on a
definition_entry that contains private constants, they are either
- inlined in the main proof term but not re-checked
- declared globally without re-checking them
As a safety measure, the opaque data type contains a pointer to the
revstruct (an internal field of safe_env that changes every time a new
constant is added), and such pointer is compared with the current value
store in safe_env when the private_constant is inlined.  Only when the
comparison is successful the private_constant is not re-checked.  Otherwise
else it is.  In short, we accept into the kernel private constant only
when they arrive in the very same order and on top of the very same env
they arrived when we fist checked them.

Note: private_constants produced by workers never pass the safety
measure (the revstruct pointer is an Ephemeron).  Sending back the
entire revstruct is possible but: 1. we lack a way to quickly compare
two revstructs, 2. it can be large.

1 files changed, 9 insertions, 8 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f7d3ad5d0..b2603315d 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -193,7 +193,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), Declareops.no_seff)
+      (c, ctx), Safe_typing.empty_private_constants)
 
 (**********************************************************************)
 (* Build the involutivity of symmetry for an inductive type           *)
@@ -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  *)
@@ -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   *)
@@ -694,7 +695,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), Declareops.no_seff)
+     (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 *)
 
@@ -782,4 +783,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, Declareops.no_seff)
+    build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Safe_typing.empty_private_constants)