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, 5 insertions, 5 deletions

diff --git a/library/declare.mli b/library/declare.mli
index 7ed451c3f..fdbd23561 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -22,7 +22,7 @@ open Decl_kinds
 (** Declaration of local constructions (Variable/Hypothesis/Local) *)
 
 type section_variable_entry =
-  | SectionLocalDef of definition_entry
+  | SectionLocalDef of Safe_typing.private_constants definition_entry
   | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
@@ -32,7 +32,7 @@ val declare_variable : variable -> variable_declaration -> object_name
 (** Declaration of global constructions 
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = constant_entry * logical_kind
+type constant_declaration = Safe_typing.private_constants constant_entry * logical_kind
 
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
@@ -49,8 +49,8 @@ type internal_flag =
 
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> 
-  ?poly:polymorphic -> ?univs:Univ.universe_context -> ?eff:Declareops.side_effects ->
-  constr -> definition_entry
+  ?poly:polymorphic -> ?univs:Univ.universe_context ->
+  ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 val declare_constant :
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
@@ -60,7 +60,7 @@ val declare_definition :
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
 
-(** Since transparent constant's side effects are globally declared, we
+(** Since transparent constants' side effects are globally declared, we
  *  need that *)
 val set_declare_scheme :
   (string -> (inductive * constant) array -> unit) -> unit