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

diff --git a/toplevel/command.ml b/toplevel/command.ml
index d75efeca1e..433ef4dccd 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -169,7 +169,7 @@ let declare_definition ident (local, p, k) ce imps hook =
     gr
   | Discharge | Local | Global ->
     declare_global_definition ident ce local k imps in
-  Lemmas.call_hook (Future.fix_exn_of ce.Entries.const_entry_body) hook local r
+  Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r
 
 let _ = Obligations.declare_definition_ref := declare_definition
 
@@ -178,7 +178,7 @@ let do_definition ident k pl bl red_option c ctypopt hook =
     if Flags.is_program_mode () then
       let env = Global.env () in
       let (c,ctx), sideff = Future.force ce.const_entry_body in
-      assert(Declareops.side_effects_is_empty sideff);
+      assert(Safe_typing.empty_private_constants = sideff);
       assert(Univ.ContextSet.is_empty ctx);
       let typ = match ce.const_entry_type with 
 	| Some t -> t
@@ -1139,7 +1139,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
-    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
+    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let ctx = Evd.universe_context ?names:pl evd in
     ignore (List.map4 (declare_fix (local, poly, Fixpoint) ctx)
 	      fixnames fixdecls fixtypes fiximps);
@@ -1169,7 +1169,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
     let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
     let vars = Universes.universes_of_constr (List.hd fixdecls) in
-    let fixdecls = List.map Term_typing.mk_pure_proof fixdecls in
+    let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in