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

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9e27ddf2e..c43932324 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -334,7 +334,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 	ignore(
 	  Declare.declare_constant
 	    name
-	    (Entries.DefinitionEntry ce,
+	    (DefinitionEntry ce,
 	     Decl_kinds.IsDefinition (Decl_kinds.Scheme))
 	);
 	Declare.definition_message name;
@@ -447,7 +447,7 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entry list =
+let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_constants definition_entry list =
   let env = Global.env () in
   let funs = List.map fst fas in
   let first_fun = List.hd funs in
@@ -541,7 +541,7 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
       let sorts = Array.of_list sorts in
       List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
-    let first_princ_body,first_princ_type = const.Entries.const_entry_body, const.Entries.const_entry_type in
+    let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in
     let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = destFix fix in
     let other_result =
@@ -585,9 +585,9 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Entries.definition_entr
 	     Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
 	   in
 	   {const with
-	      Entries.const_entry_body = 
-                (Future.from_val (Term_typing.mk_pure_proof princ_body));
-	      Entries.const_entry_type = Some scheme_type
+	      const_entry_body = 
+                (Future.from_val (Safe_typing.mk_pure_proof princ_body));
+	      const_entry_type = Some scheme_type
 	   }
       )
       other_fun_princ_types
@@ -620,7 +620,7 @@ let build_scheme fas =
        ignore
 	 (Declare.declare_constant
 	    princ_id
-	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+	    (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
        Declare.definition_message princ_id
     )
     fas