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.

5 files changed, 25 insertions, 24 deletions

diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index e6a8cbe3ad..8a6d93cf7c 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -52,7 +52,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind =
     let ctxset = Univ.ContextSet.of_context ctx in
     let ectx = Evd.evar_universe_context_of ctxset in
     let sigma, c = build_induction_scheme env (Evd.from_ctx ectx) (ind,u) dep sort in
-      (c, Evd.evar_universe_context sigma), Declareops.no_seff
+      (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants
 
 let build_induction_scheme_in_type dep sort ind =
   let env = Global.env () in
@@ -68,15 +68,15 @@ let build_induction_scheme_in_type dep sort ind =
  
 let rect_scheme_kind_from_type =
   declare_individual_scheme_object "_rect_nodep"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let rect_scheme_kind_from_prop =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
-    (fun _ x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let rect_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
-    (fun _ x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
+    (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
 let ind_scheme_kind_from_type =
   declare_individual_scheme_object "_ind_nodep"
@@ -109,24 +109,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
 
 let case_scheme_kind_from_type =
   declare_individual_scheme_object "_case_nodep"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let case_scheme_kind_from_prop =
   declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
-  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_type =
   declare_individual_scheme_object "_case" ~aux:"_case_from_type"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_type_in_prop =
   declare_individual_scheme_object "_casep_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_prop =
   declare_individual_scheme_object "_case_dep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants)
 
 let case_dep_scheme_kind_from_prop_in_prop =
   declare_individual_scheme_object "_casep"
-  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
+  (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index f7d3ad5d0a..b2603315d5 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)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 6bb84808a9..3fe3307308 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -25,7 +25,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 * Declareops.side_effects
+  constr Evd.in_evar_universe_context * Safe_typing.private_constants
 val build_r2l_forward_rew_scheme :
   bool -> env -> inductive -> sorts_family -> constr Evd.in_evar_universe_context
 val build_l2r_forward_rew_scheme :
@@ -37,7 +37,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 * Declareops.side_effects
+  constr Evd.in_evar_universe_context * Safe_typing.private_constants
 val sym_involutive_scheme_kind : individual scheme_kind
 
 (** Builds a congruence scheme for an equality type *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bc711b81ef..674c85af79 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -317,7 +317,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
 	assert false
     in
       let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
-	sigma, elim, Declareops.no_seff
+	sigma, elim, Safe_typing.empty_private_constants
   else
   let scheme_name = match dep, lft2rgt, inccl with
     (* Non dependent case *)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1437b24625..0b920066fd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4455,9 +4455,9 @@ let abstract_subproof id gk tac =
   (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
   let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
   let evd = Evd.set_universe_context evd ectx in
-  let open Declareops in
-  let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
-  let effs = cons_side_effects eff
+  let open Safe_typing in
+  let eff = private_con_of_con (Global.safe_env ()) cst in
+  let effs = add_private eff
     Entries.(snd (Future.force const.const_entry_body)) in
   let args = List.rev (instance_from_named_context sign) in
   let solve =